0 
n=1
1 else fib(n-1)+fib(n-2) fi (recursive)
n:
. fib(n) 
q == if p true else q fip,q:
. (p q) j == if i=j true ; false fii,j:
. (i=j) == {i:| 0
i } Type
A == A 
FalseA:Prop. (A) Prop| Some definitions of interest. | |
| fib | 0 n=1 1 else fib(n-1)+fib(n-2) fi (recursive) |
| n:. fib(n) | |
| bor | q == if p true else q fi |
| p,q:. (p q) | |
| eq_int | j == if i=j true ; false fi |
| i,j:. (i=j) | |
| nat | == {i:| 0i } |
| Type | |
| not | A == A False |
| A:Prop. (A) Prop |
About:
 |  |  |  |  |  |  |
 |  |  |  |
 |  |  |  |  |  |  |