Agda

Samuel Mimram

1 The syntax of Agda

This is a quick reminder, for more details have a look at the Agda documentation.

1.1 Main shortcuts

Shortcut Effect
C-c C-l typecheck and highlight the current file
C-c C-, get information about the hole under the cursor
C-c C-. show both the type of the current hole and of the proposed filling
C-c C-space give a solution
C-c C-c case analysis on a variable (≈ an elimination rule)
C-c C-r refine the hole (≈ an introduction rule)
C-c C-a automatic fill
middle click definition of the term

1.2 UTF-8 symbols

∧ \and ⊤ \top → \to
∨ \or ⊥ \bot ¬ \neg
∀ \all Π \Pi λ \Gl
∃ \ex Σ \Sigma ≡ \Equiv
ℕ \bN × \times ≤ \le
∈ \in ⊎ \uplus ∷ \::
∎ \qed ₁ \_1 ⇒ \=>
⟨ \< ⟩ \>

1.3 Comments

-- This is a comment
{-
This is
a multiline
comment
-}

1.4 Importing functions

We can import all the definitions from ModuleName.agda with

open import ModuleName

1.5 Declaring a function

pred : ℕ → ℕ
pred zero = zero
pred (suc n) = n

1.6 Capturing an optional argument

id : {ℓ : Level} {A : Type ℓ} → A → A
id {ℓ} {A} a = a

Named captures are also supported:

id : {ℓ : Level} {A : Type ℓ} → A → A
id {A = A} a = a