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
A == 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 | |
| not | A == A False |
| A:Prop. (A) Prop |
About:
 |  |  |  |  |  |  |
 |  |  |  |  |  |
 |  |  |  |  |  |  |