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)

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

Runtimes (2)