b == if b
True else False fi
b:
. b 
Prop
== {i:
| 0
i } Type SB == 
B<Ai,j:. (ij) Prop
n then 0 else m-n fi m,n:. nnsub(m;n) j == if i<j true ; false fii,j:. (i<j) A == A 
FalseA:Prop. (A) Prop| Some definitions of interest. | |
| assert | b == if b True else False fi |
| b:. b Prop | |
| nat | == {i:| 0i } |
| Type | |
| S | |
| le | B == B<A |
| i,j:. (ij) Prop | |
| nnsub | n then 0 else m-n fi |
| m,n:. nnsub(m;n) | |
| lt_int | j == if i<j true ; false fi |
| i,j:. (i<j) | |
| not | A == A False |
| A:Prop. (A) Prop |
About:
 |  |  |  |  |  |  |  |  |  |
 |  |  |  |  |  |  |  |  |