# Agda Template

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

`module HelloAgda where`

`import Relation.Binary.PropositionalEquality as Eq`

`open Eq using (_≡_; refl)`

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

`data ℕ : Set where`

` zero : ℕ`

` suc : ℕ → ℕ`

`_+_ : ℕ → ℕ → ℕ`

`zero + n = n`

`(suc m) + n = suc (m + n)`

0.9s

Agda (agda)

## Interactive Theorem Proving

With `Tab`

and `Shift-Tab`

you can get assistance from Agda in providing terms of the correct type. In the following example you can start typing a `plus a b = ?`

and hit Tab to get a list of suggestions. Choosing the *hole* expression `{! !}`

you can further refine your goal, or ask agda to split your definition on a variable for pattern matching hitting Tab again with the cursor after the hole:

`module AgdaInteraction where`

`data N : Set where`

` z : N`

` suc : N → N`

` `

`_⊹_ : N → N → N`

`a ⊹ b = {! a !}`

1.0s

Agda (agda)

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 via Agda Jupyter Kernel. Unicode input method is triggered via typing a first `\`

and follows emacs agda mode translations.