| Some definitions of interest. |
|
sfa_doc_ntuple | Def A^n == if n=0 Unit ; n=1 A else A(A^(n-1)) fi (recursive) |
| | Thm* A:Type, n:. (A^n) Type |
|
eq_int | Def i=j == if i=j true ; false fi |
| | Thm* i,j:. (i=j) |
|
ge | Def ij == ji |
| | Thm* i,j:. (ij) Prop |
|
nat | Def == {i:| 0i } |
| | Thm* Type |