| Some definitions of interest. |
|
int_iseg | Def {i...j} == {k:| ik & kj } |
| | Thm* i,j:. {i...j} Type |
|
lt_int | Def i<j == if i<j true ; false fi |
| | Thm* i,j:. (i<j) |
|
nat | Def == {i:| 0i } |
| | Thm* Type |
|
not | Def A == A False |
| | Thm* A:Prop. (A) Prop |
|
sq_type | Def SQType(T) == x,y:T. x = y {x ~ y} |
|
top | Def Top == Void(given Void) |
| | Thm* Top Type |