WhoCites Definitions NuprlPrimitives Sections NuprlLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Who Cites sfa doc sexpr cases?
sfa_doc_sexpr_casesDef Case of s :  Inj(x g(x) ; Cons(s1;s2 f(s1;s2)
Def == InjCase(ss1s2s1s2/s1,s2f(s1;s2); xg(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:Case of s :  Inj(x g(x) ; Cons(s1;s2 f(s1;s2) has structure: sfa_doc_sexpr_cases(ss1,s2.f(s1;s2); x.g(x))

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

WhoCites Definitions NuprlPrimitives Sections NuprlLIB Doc