Stack-based syntax

A definition's body can be built clause-by-clause from three tactics: \elim, \intro, and \split.

`\elim`

\elim names an argument already in scope and case-splits on it. Clauses must list every constructor of the eliminated type.

\let add : (m n : Nat) -> Nat \where
  add m n <= \elim m
  | add zero n => n
  | add (suc m) n => suc (add m n)

Example: `sym` on propositional equality

\let sym {A : 𝓤} {x y : A} : x = y -> y = x \where
  sym p <= \elim p
  | sym refl => refl

`\intro`

\intro pulls the next pi-bound argument from the signature into scope as a variable. Each clause then spells out the fully-applied left-hand side. This is not working well with implicit for now.

\let identity (A : 𝓤) : A -> A \where
  <= \intro
  | identity A x => x

`\split`

\split case-splits the topmost introduced argument. It is normally chained right after \intro.

\let neg : Bool -> Bool \where
  <= \intro
  <= \split
  | neg true => false
  | neg false => true

You can write the same function with \elim

\let neg : Bool -> Bool \where
  neg b <= \elim b
  | neg true => false
  | neg false => true