Def Size(s) == Case of s :  Inj(x)  1 ; Cons(s1;s2)  Size(s1)+Size(s2)
Def (recursive)

is mentioned by

Thm* Size(Cons(Inj(1);Cons(Inj(2);Inj(1)))) = 3	[sfa_doc_sexpr_size_example]
Thm* A:Type, s:Sexpr(A). Size(s) = 1    sexprAtom(s)  A	[sfa_doc_sexpr_atom_wf]
Thm* s:Sexpr(A). Size(s)  1    Size(sexprCdr(s))<Size(s)	[sfa_doc_sexprcdrsize]
Thm* s:Sexpr(A). Size(s)  1    Size(sexprCar(s))<Size(s)	[sfa_doc_sexprcarsize]

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html