{"size": 1034, "ext": "scrbl", "max_stars_repo_path": "scribble-minted-lib/examples/agda-example.scrbl", "max_stars_repo_name": "wilbowma/scribble-minted", "max_stars_repo_stars_event_min_datetime": "2019-02-16T06:16:34.000Z", "max_stars_repo_stars_event_max_datetime": "2021-03-30T13:39:10.000Z", "max_issues_repo_path": "scribble-minted-lib/examples/agda-example.scrbl", "max_issues_repo_name": "wilbowma/scribble-minted", "max_issues_repo_issues_event_min_datetime": "2019-02-26T04:22:53.000Z", "max_issues_repo_issues_event_max_datetime": "2021-04-03T06:28:41.000Z", "max_forks_repo_path": "scribble-minted-lib/examples/agda-example.scrbl", "max_forks_repo_name": "wilbowma/scribble-minted", "max_forks_repo_forks_event_min_datetime": null, "max_forks_repo_forks_event_max_datetime": null}
{"max_stars_count": 15, "max_issues_count": 6, "max_forks_count": null, "avg_line_length": 28.7222222222, "max_line_length": 63, "alphanum_fraction": 0.7959381044}
#lang scribble/manual

@require[scribble/minted]

@(current-pygmentize-default-style 'manni)

@title{Demo: Agda in Action}

This chapter contains a brief demonstration of Agda,
the language used in PLFA and in CS 747.
I won't be explaining everything in detail,
and you shouldn't expect to understand everything fully.
We'll go over everything more carefully later.

Interactions with Agda take place within the text editor Emacs,
using short keyboard sequences.
One sequence brings in the demonstration file
(@tt{demo.agda}, linked on the Handouts page;
we're using the starter version)
and another activates Agda,
checking syntax and providing highlighting.

The file starts with these lines:

@minted["agda"]|{
module demo where

open import Relation.Binary.PropositionalEquality
open import Data.Nat
}|

These lines start the module defined by the file,
and import library code for using equality and natural numbers.
These very basic notions are not built into Agda;
they are constructed, and later we will see how this is done.
