typical
Basic Syntax
-
data(inductive type)
(data Nat [zero : Nat] [suc : (Nat . -> . Nat)])
-
define
introduces user-defined variables; define `a` is `zero` (define a : Nat zero)
-
check type of term
; read as "check `zero` is a `Nat`?" (check zero : Nat)
TODO
- strictly positive of data type
- dependent function