| Some definitions of interest. |
|
exponentiation | Def n^k == if k=0 1 else n(n^(k-1)) fi (recursive) |
| | Thm* n:, k:. (n^k) |
| | Thm* n,k:. (n^k) |
| | Thm* n:, k:. (n^k) |
|
eq_int | Def i=j == if i=j true ; false fi |
| | Thm* i,j:. (i=j) |
|
not | Def A == A False |
| | Thm* A:Prop. (A) Prop |