| Some definitions of interest. |
|
assert | Def b == if b True else False fi |
| | Thm* b: . b Prop |
|
last | Def last(L) == L[(||L||-1)] |
| | Thm* T:Type, L:T List. null(L)  last(L) T |
|
le | Def A B == B<A |
| | Thm* i,j: . (i j) Prop |
|
length | Def ||as|| == Case of as; nil 0 ; a.as' ||as'||+1 (recursive) |
| | Thm* A:Type, l:A List. ||l||  |
| | Thm* ||nil||  |
|
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)  |