# Agda Template

Remix or try out this notebook to get started with Agda, check the notes below about interaction limitations. The first cell of an Agda Runtime must start with a module declaration (optionally preceded by pragmas with options) and this will be subject to Agda module naming conventions when imported in other runtimes.

`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`
`  ∎`
5.7s
Agda Runtime (Agda)

And if you feel you're in that HoTT mood, give Cubical a try:

`{-# OPTIONS --cubical #-}`
`module CubiTest {ℓ} where`
`open import Cubical.Core.Primitives`
`  hiding (_≡_)`
`postulate`
`  ℐ : I → Set ℓ`
`  a₀ : (ℐ i0)`
`  a₁ : (ℐ i1)`
`-- PathP : (ℐ : I → Set ℓ) → (ℐ i0) → (ℐ i1) → Set ℓ`
`-- intro and elim`
`PathP⁺ : (f : (i : I) → (ℐ i)) → PathP ℐ (f i0) (f i1)`
`PathP⁺ f = λ i → f i`
`PathP⁻ : (p : PathP ℐ a₀ a₁) → (r : I) → (ℐ r)`
`PathP⁻ p r = p r`
`_≡_ : {A : Set ℓ} → A → A → Set ℓ`
`_≡_ {A} = PathP (λ _ → A)`
`funExt : {A : Set ℓ} → {B : A → Set ℓ} →`
`         {f g : (x : A) → B x} →`
`         (p : (x : A) → f x ≡ g x) → f ≡ g`
`funExt p i = λ x → (p x) i`
0.7s
cubical library testCubical Agda (Agda)

## Interactive Theorem Proving in Nextjournal

Since our runtimes are powered by an Agda Jupyter Kernel, we can support only a limited subset of Emacs Agda mode and interaction.

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 = ?`
0.7s
Agda Runtime (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.