WhoCites Definitions prog 1 Sections StandardLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Who Cites case pattern1?
case_pattern1Def <<"a", b>, c, 1> => body(b;ccont(x,z)
Def == x/x2,x1.
Def == x2/x2@0,x1@0.
Def == InjCase(if x2@0="a"Atominl(*); inr(*) fi
Def == InjCasex1/x2@1,x1@1.
Def == InjCase; InjCase(if x1@1=1 inl(*) ; inr(*) fi
Def == InjCase; InjCasebody(x1@0;x2@1)
Def == InjCase; InjCasecont(z,z))
Def == InjCasecont(z,z))

Syntax:<<"a", b>, c, 1> =>
<<"abody(b;c)
cont
has structure: case_pattern1(b,c.body(b;c); cont)

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

WhoCites Definitions prog 1 Sections StandardLIB Doc