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

  ∎

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

follow the environment links to see how they're built.

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 = ?

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.