typical

Basic Syntax

1. data(inductive type)

   (data Nat
       [zero : Nat]
       [suc : (Nat . -> . Nat)])

2. define introduces user-defined variables

   ; define `a` is `zero`
   (define a : Nat
     zero)

3. check type of term

   ; read as "check `zero` is a `Nat`?"
   (check zero : Nat)

TODO

• strictly positive of data type
• dependent function