b == if b
True else False fi
b:
. b 
Prop 0 else 1+mu(
x.f(1+x)) fi (recursive) {f:(
)| 
x:. f(x) } == {i:
| 0
i } Type
b T == 
a = b TA:Type, x,y:A. (x y) PropA == A 
FalseA:Prop. (A) Prop| Some definitions of interest. | |
| assert | b == if b True else False fi |
| b:. b Prop | |
| kleene_minimize | 0 else 1+mu(x.f(1+x)) fi (recursive) |
| {f:()| x:. f(x) } | |
| nat | == {i:| 0i } |
| Type | |
| nequal | b T == a = b T |
| A:Type, x,y:A. (x y) Prop | |
| not | A == A False |
| A:Prop. (A) Prop |
About:
 |  |  |  |  |  |  |
 |  |  |  |  |  |
 |  |  |  |  |  |  |
 |