Agda Template

Remix this to get started with Agda (v2.6.1).

module HelloAgda where

import Relation.Binary.PropositionalEquality as Eq

open Eq using (_≡_)

open Eq.≡-Reasoning using (begin_;_≡⟨⟩_;_∎)

data ℕ : Set where

  zero : ℕ

  suc : ℕ → ℕ

{-# BUILTIN NATURAL ℕ #-}

_+_ : ℕ → ℕ → ℕ

0 + n = n

suc n + m = suc (n + m)

_ : 1 + 1 ≡ 2

_ = begin 

  suc 0 + 1

  ≡⟨⟩

  suc (0 + 1)

  ≡⟨⟩

  suc 1

  ≡⟨⟩

  2

  ∎

Interactive Theorem Proving

With Tab and Shift-Tab (in a running Agda runtime) you can get assistance in providing terms of the correct type, placing the cursor next to a ? or a hole {! !}. In the following example you can hit Tab at the end of the code to obtain a list of suggestions

data Vec (A : Set) : ℕ → Set where

  [] : Vec A zero

  _::_ : ∀ {n} (x : A) (xs : Vec A n) → Vec A (suc n)

hd : {A : Set} → {n : ℕ} → Vec A (suc n) → A

hd x = ?

Choosing the hole expression {! !} you can further refine your goal, or ask Agda to split your definition on a variable for pattern matching by typing it inside the hole:

hd : {A : Set} → {n : ℕ} → Vec A (suc n) → A

hd x = {! x !}

now hitting Tab again with the cursor on the right of the hole should suggest to replace the above with a constructor expression, like so

hd : {A : Set} → {n : ℕ} → Vec A (suc n) → A

hd (x :: x₁) = ?

now pressing Tab again after ? we'll be suggested to replace an x for ? and this will already type check fine. We can also go further and ask Agda to split on the variable x₁ instead, by inserting it into the hole, i.e. turn

hd : {A : Set} → {n : ℕ} → Vec A (suc n) → A

hd (x :: x₁) = {! x₁ !}

into

hd : {A : Set} → {n : ℕ} → Vec A (suc n) → A

hd (x :: []) = ?

hd (x :: (x₁ :: x₂)) = ?

and so on.

With Shift+Tab while the cursor is next to ? or a hole, you'll get a summary of the current goals and their types. Code execution and completions is handled by (our fork of) Agda Jupyter Kernel. Unicode input method is triggered via typing a first \ and follows emacs agda mode translations.