0
Unit ; n=1 A else A
(A^(n-1)) fi (recursive)
A:Type, n:
. (A^n) 
Typej == if i=j true ; false fii,j:
. (i=j) 
== {i:| 0
i } TypeX:A. X B) & (X:B. X A)| Some definitions of interest. | |
| sfa_doc_ntuple | 0 Unit ; n=1 A else A(A^(n-1)) fi (recursive) |
| A:Type, n:. (A^n) Type | |
| eq_int | j == if i=j true ; false fi |
| i,j:. (i=j) | |
| nat | == {i:| 0i } |
| Type | |
| sfa_doc_exteq | X:A. X B) & (X:B. X A) |
About:
 |  |  |  |  |  |  |  |
 |  |  |  |
 |  |  |  |  |  |