| | Some definitions of interest. |
|
| assert | Def  b == if b True else False fi |
| | | Thm*  b: . b  Prop |
|
| hequal | Def equal ==  x:'a. y:'a. x = y |
| | | Thm* 'a:S. equal ('a   'a hbool) |
|
| bequal | Def x = y ==  (x = y T) |
| | | Thm* T:Type, x,y:T. (x = y) |
|
| hfun | Def 'a 'b == 'a'b |
| | | Thm* 'a,'b:S. ('a 'b) S |
|
| hlet | Def let == f:'a'b. e:'a. let x = e in f(x) |
| | | Thm* 'a,'b:S. let (('a 'b) 'a 'b) |
|
| let | Def let x = a in b(x) == (x.b(x))(a) |
| | | Thm* A,B:Type, a:A, b:(AB). let x = a in b(x) B |
|
| stype | Def S == {T:Type|  x:T. True } |
| | | Thm* S Type{2} |
|
| tlambda | Def (x:T. b(x))(x) == b(x) |
