| Some definitions of interest. |
|
assert | Def b == if b True else False fi |
| | Thm* b: . b Prop |
|
l_member | Def (x l) == i: . i<||l|| & x = l[i] T |
| | Thm* T:Type, x:T, l:T List. (x l) Prop |
|
not | Def A == A  False |
| | Thm* A:Prop. ( A) Prop |
|
null | Def null(as) == Case of as; nil true ; a.as' false |
| | Thm* T:Type, as:T List. null(as)  |
| | Thm* null(nil)  |