| | Some definitions of interest. |
|
| harb | Def arb == arb('a) |
| | | Thm*  'a:S. arb  'a |
|
| hres_abstract | Def res_abstract ==  P:'a   . f:'a'b. res_lambda('a;'b;x.P(x);x.f(x)) |
| | | Thm* 'a,'b:S. res_abstract (('a hbool) ('a 'b) 'a 'b) |
|
| res_lambda | Def res_lambda('a;'b;x.P(x);x.f(x)) == x:'a. if P(x) then f(x) else arb('b) fi |
| | | Thm* 'a,'b:S, P:('a), f:('a'b). res_lambda('a;'b;x.P(x);x.f(x)) 'a'b |
|
| arb | Def arb(T) == InjCase(lem(T); x. x, "uu") |
| | | Thm* T:S. arb(T) T |
|
| hall | Def all == p:'a.  x:'a. (p(x)) |
| | | Thm* 'a:S. all (('a hbool) hbool) |
|
| assert | Def  b == if b True else False fi |
| | | Thm* b:. b Prop |
|
| hcond | Def cond == b:. p:'a. q:'a. if b then p else q fi |
| | | Thm* 'a:S. cond (hbool 'a 'a 'a) |
|
| bif | Def bif(b; bx.x(bx); by.y(by)) == if b x(*) else y(x.x) fi |
| | | Thm* A:Type, b:, x:(bA), y:(( b)A). bif(b; bx.x(bx); by.y(by)) A |
|
| hbool | Def hbool == |
| | | Thm* hbool S |
|
| hequal | Def equal == x:'a. y:'a. x = y |
| | | Thm* 'a:S. equal ('a 'a hbool) |
|
| hfun | Def 'a 'b == 'a'b |
| | | Thm* 'a,'b:S. ('a 'b) S |
|
| stype | Def S == {T:Type|  x:T. True } |
| | | Thm* S Type{2} |
|
| tlambda | Def (x:T. b(x))(x) == b(x) |
