data-type
data
8.2

data-type

Lîm Tsú-thuàn

 (require data-type) package: data-type

syntax

(data type-name
      clause ...)
 
clause = [name param ...]
     
param = type
  | [param-name type]
usage

(data expr
  [Var (name : Symbol)]
  [abs (name : Symbol) (body : expr)]
  [app (fn : expr) (arg : expr)]
  [pi (name : Symbol) (e : expr) (body : expr)]
  [type (level : Integer)]
  [nat]
  [zero]
  [succ (n : expr)]
  [rec expr expr expr expr]
  [id expr expr expr]
  [refl expr]
  [J expr expr expr expr expr expr])