1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19
type tm = | Var of int | Pi of tm * (* BINDS *) tm | Lam of (* BINDS *) tm | App of tm * tm | Sg of tm * (* BINDS *) tm | Pair of tm * tm | Fst of tm | Snd of tm | Type | Bool | True | False | BoolElim of { motive : (* BINDS *) tm; true_case : tm; false_case : tm; scrut : tm; }