| | Some definitions of interest. |
|
| hall | Def all ==  p:'a   .   x:'a. (p(x)) |
| | | Thm* 'a:S. all  (('a hbool) hbool) |
|
| ball | Def x:T. P(x) ==  (x:T.  P(x)) |
| | | Thm* T:Type, P:(T). (x:T. P(x)) |
|
| hselect | Def select == p:'a. @x:'a. (p(x)) |
| | | Thm* 'a:S. select (('a hbool) 'a) |
|
| bchoose | Def @x:'a. p(x) == @x:'a. p(x) |
| | | Thm* 'a:S, p:('a). (@x:'a. p(x)) 'a |
|
| assert | Def b == if b True else False fi |
| | | Thm* b:. b Prop |
|
| hequal | Def equal == x:'a. y:'a. x = y |
| | | Thm* 'a:S. equal ('a 'a hbool) |
|
| bequal | Def x = y == (x = y T) |
| | | Thm* T:Type, x,y:T. (x = y) |
|
| hnot | Def not == p:.   p |
| | | Thm* not (hbool hbool) |
|
| bnot | Def b == if b false else true fi |
| | | Thm* b:. b |
|
| hzero_rep | Def zero_rep == @x: . (y:. x = suc_rep(y) ) |
| | | Thm* zero_rep hind |
|
| hsuc_rep | Def suc_rep == x:. (@f:. (one_one(;;f) & onto(;;f)))(x) |
| | | Thm* suc_rep (hind hind) |
|
| choose | Def @x:T. P(x) == InjCase(lem({x:T| P(x) }); x. x, arb(T)) |
| | | Thm* T:S, P:(TType). (@x:T. P(x)) T |
|
| hind | Def hind == |
| | | Thm* hind S |
|
| nat | Def == {i: | 0 i } |
| | | Thm* Type |
| | | Thm* S |
|
| not | Def A == A   False |
| | | Thm* A:Prop. (A) Prop |
|
| tlambda | Def (x:T. b(x))(x) == b(x) |
