Definitions StandardLib Sections NuprlLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
No other cites to report in StandardLib
case_pattern2Def <a, inl <<"a", b>, c, 1>> => body(a;b;ccont(x,z)
Def == x/x2,x1.
Def == InjCase(x1
Def == InjCasex1@0x1@0/x2@0,x1@1.
Def == InjCase; x1@0x2@0/x2@0,x1@2.
Def == InjCase; x1@0InjCase(if x2@0="a"Atominl(*); inr(*) fi
Def == InjCase; x1@0. InjCasex1@1/x2@1,x1@1.
Def == InjCase; x1@0. InjCase; InjCase(if x1@1=1 inl(*) ; inr(*) fi
Def == InjCase; x1@0. InjCase; InjCasebody(x2;x1@2;x2@1)
Def == InjCase; x1@0. InjCase; InjCasecont(z))
Def == InjCase; x1@0. InjCasecont(z))
Def == InjCase_cont(z))

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

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

Definitions StandardLib Sections NuprlLIB Doc