NuprlPrimitives
Sections
NuprlLIB
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Def
sexprCar(
s
) == Case of
s
: Inj(
x
)
Inj(
x
) ; Cons(
s1
;
s2
)
s1
is mentioned by
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
NuprlPrimitives
Sections
NuprlLIB
Doc
Inj(x) ; Cons(s1;s2) s1 Inj(x) ; Cons(s1;s2) s1
s:Sexpr(A). Size(s) 
1 
Size(sexprCar(s))<Size(s)