A workshop on learning Agda with minimal prerequisites.
A workshop on learning Agda with minimal prerequisites.
The exercises are written for Agda 2.5.1.
You may find stack
more reliable than cabal
to build Agda.
stack install --resolver nightly-2016-05-08 Agda
agda-mode setup
I created a Docker image with Agda, Emacs and the exercises. See scottfleischman/agda-from-nothing
docker run -it scottfleischman/agda-from-nothing
Note The Mac Terminal has issues sending common control sequences such as Control+Comma. It may be better to do a full install as above, or use Docker with Agda as below with a local editor and agda-mode.
See banacorn/docker-agda.
See the Agda docs for all of the keybindsings. Here are ones I commonly use. Note C-
means Control+
.
\r-
or \to
for →
\==
for ≡
\==n
for ≢
\all
for ∀
\<=
for ≤
\<=n
for ≰
\ell
for ℓ
\lambda
or \Gl
for λ
\'
for ′
\::
for ∷
(it looks like two colons, but it is a single Unicode character)\_0
for ₀
(subscript 0)\_1
for ₁
(and so on)\^0
for ⁰
(superscript 0)\^1
for ¹
(and so on)\in
for ∈
\ni
for ∋
\lub
for ⊔
(least upper bound; max)\Pi
for Π
\Sigma
or \GS
for Σ
C-u C-x Equals