| | Some definitions of interest. |
|
| absval | Def |i| == if 0  i i else -i fi |
| | | Thm*  x: . |x|   |
|
| iff | Def P   Q == (P  Q) & (P Q) |
| | | Thm* A,B:Prop. (A B) Prop |
|
| imax | Def imax(a;b) == if ab b else a fi |
| | | Thm* a,b:. imax(a;b) |
|
| imin | Def imin(a;b) == if ab a else b fi |
| | | Thm* a,b:. imin(a;b) |
|
| int_lower | Def {...i} == {j:| ji } |
| | | Thm* i:. {...i} Type |
|
| int_nzero | Def   == {i:| i  0 } |
| | | Thm* Type |
|
| int_seg | Def {i..j} == {k:| i k < j } |
| | | Thm* m,n:. {m..n} Type |
|
| nat | Def == {i:| 0i } |
| | | Thm* Type |
|
| le | Def AB ==  B<A |
| | | Thm* i,j:. (ij) Prop |
|
| nat_plus | Def  == {i:| 0<i } |
| | | Thm* Type |
