T)+A)
A:Type. Sexpr(A) 
TypeDef == Case of e
Def == CaInj(x)
Inj(x)
Def == CaCons(s1;s2)
Cons(Reverse(s2);Reverse(s1))
Def (recursive)
A:Type, e:Sexpr(A). Reverse(e) Sexpr(A)| Some definitions of interest. | |
| sfa_doc_sexpr | T)+A) |
| A:Type. Sexpr(A) Type | |
| sfa_doc_sexpr_reverse | Def == Case of e Def == CaInj(x) Inj(x)
Def == CaCons(s1;s2) Cons(Reverse(s2);Reverse(s1))
Def (recursive) |
| A:Type, e:Sexpr(A). Reverse(e) Sexpr(A) |
About:
 |  |  |  |  |  |  |  |