No other cites to report in NuprlPrimitives
sfa_doc_sexpr_atom	Def sexprAtom(s) == Case of s :  Inj(x)  x ; Cons(s1;s2)  0
	Thm* A:Type, s:Sexpr(A). Size(s) = 1    sexprAtom(s)  A
sfa_doc_sexpr_cases	Def Case of s :  Inj(x)  g(x) ; Cons(s1;s2)  f(s1;s2) Def == InjCase(s; s1s2. s1s2/s1,s2. f(s1;s2); x. g(x))
	Thm* A:Type, C:(Sexpr(A)Type), s:Sexpr(A), Thm* f:(s1,s2:Sexpr(A)C(Cons(s1;s2))), g:(x:AC(Inj(x))). Thm* (Case of s :  Inj(x)  g(x) ; Cons(s1;s2)  f(s1,s2))  C(s)

Syntax:

sexprAtom(s)

has structure:

sfa_doc_sexpr_atom(s)

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