n then 0 else m-n fi 
m,n:
. nnsub(m;n) 
x(*) else y(
x.x) fiA:Type, b:
, x:(b
A), y:((
b)A). bif(b; bx.x(bx); by.y(by)) A == {i:
| 0
i } Type SB == B<Ai,j:. (ij) Propj == if i<j true ; false fii,j:. (i<j) | Some definitions of interest. | |
| nnsub | n then 0 else m-n fi |
| m,n:. nnsub(m;n) | |
| bif | x(*) else y(x.x) fi |
| A:Type, b:, x:(bA), y:((b)A). bif(b; bx.x(bx); by.y(by)) A | |
| nat | == {i:| 0i } |
| Type | |
| S | |
| le | B == B<A |
| i,j:. (ij) Prop | |
| lt_int | j == if i<j true ; false fi |
| i,j:. (i<j) |
About:
 |  |  |  |  |  |  |  |  |  |
 |  |  |  |  |  |  |  |  |