== {i:
| 0<i } 
Type
T)+A)
A:Type. Sexpr(A) Type
1 ; Cons(s1;s2) Size(s1)+Size(s2)
Def (recursive)
A:Type, s:Sexpr(A). Size(s) | Some definitions of interest. | |
| nat_plus | == {i:| 0<i } |
| Type | |
| sfa_doc_sexpr | T)+A) |
| A:Type. Sexpr(A) Type | |
| sfa_doc_sexpr_size | 1 ; Cons(s1;s2) Size(s1)+Size(s2)
Def (recursive) |
| A:Type, s:Sexpr(A). Size(s) |
About:
 |  |  |  |  |  |  |
 |  |  |  |  |
 |