Def == (
x',x'':'b. rep(x') = rep(x'') 
'a 
x' = x'')
Def == & (
x:'a. 
(P(x)) 
(
x':'b. x = rep(x')))'a,'b:Type, P:('a
), rep:('b'a). type_definition('a;'b;P;rep) Propb == if b
True else False fib:. b Prop
x:T. b(x))(x) == b(x)| Some definitions of interest. | |
| type_definition | Def == ( x',x'':'b. rep(x') = rep(x'') 'a x' = x'')
Def == & ( x:'a. (P(x)) (x':'b. x = rep(x'))) |
| 'a,'b:Type, P:('a), rep:('b'a). type_definition('a;'b;P;rep) Prop | |
| assert | b == if b True else False fi |
| b:. b Prop | |
| tlambda | x:T. b(x))(x) == b(x) |
About:
 |  |  |  |  |  |  |  |  |
 |  |  |  |  |  |  |