# 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
  ∎
4.8s
Agda (Agda)

## 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 = ?
1.0s
Agda (Agda)

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 !}
Agda

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₁) = ?
Agda

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₁ !}
Agda

into

hd : {A : Set} → {n : ℕ} → Vec A (suc n) → A
hd (x :: []) = ?
hd (x :: (x₁ :: x₂)) = ?
Agda

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.