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)
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 !}
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.

Runtimes (1)
Runtime Languages (1)