| Some definitions of interest. |
|
bchoose | Def @ x:'a. p(x) == @x:'a. p(x) |
| | Thm* 'a:S, p:('a  ). (@ x:'a. p(x)) 'a |
|
bif | Def bif(b; bx.x(bx); by.y(by)) == if b x(*) else y( x.x) fi |
| | Thm* A:Type, b: , x:(b A), y:(( b) A). bif(b; bx.x(bx); by.y(by)) A |
|
int_seg | Def {i..j } == {k: | i k < j } |
| | Thm* m,n: . {m..n } Type |
|
lt_int | Def i< j == if i<j true ; false fi |
| | Thm* i,j: . (i< j)  |
|
nat | Def == {i: | 0 i } |
| | Thm* Type |
| | Thm* S |
|
stype | Def S == {T:Type| x:T. True } |
| | Thm* S Type{2} |
|
tlambda | Def ( x:T. b(x))(x) == b(x) |