0
1 else n
(n^(k-1)) fi (recursive)
n:
, k:
. (n^k) 
n,k:. (n^k) n:
, k:. (n^k) j == if i=j true ; false fii,j:. (i=j) 
== {i:| 0
i } Type == {i:| 0<i } Type
A == A 
FalseA:Prop. (A) Prop| Some definitions of interest. | |
| exponentiation | 0 1 else n(n^(k-1)) fi (recursive) |
| n:, k:. (n^k) | |
| n,k:. (n^k) | |
| n:, k:. (n^k) | |
| eq_int | j == if i=j true ; false fi |
| i,j:. (i=j) | |
| nat | == {i:| 0i } |
| Type | |
| nat_plus | == {i:| 0<i } |
| Type | |
| not | A == A False |
| A:Prop. (A) Prop |
About:
 |  |  |  |  |  |  |  |
 |  |  |  |
 |  |  |  |  |  |  |