i}(<0,0>)
0
<0,x+1> else <x+1,y-1> fi j == if i=j true ; false fi
i,j:
. (i=j) 
== {i:| 0
i } Type
A == A 
FalseA:Prop. (A) Prop| Some definitions of interest. | |
| nat_to_nat_pair | i}(<0,0>) |
| | |
| next_nat_pair | 0 <0,x+1> else <x+1,y-1> fi |
| | |
| 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:
 |  |  |  |  |  |  |
 |  |  |  |  |  |  |
 |  |  |  |  |  |  |
 |