Definitions MarkB generic Sections NuprlLIB Doc

No other cites to report in MarkB_generic
case_pattern1Def < < "a", b > , c, 1 > = > body(b;c) cont(x,z) == x/x2,x1. x2/x2@0,x1@0. InjCase(if x2@0="a"Atominl(*); inr(*) fi ; x1/x2@1,x1@1. InjCase(if x1@1=1 inl(*) ; inr(*) fi ; body(x1@0;x2@1); cont(z,z)); cont(z,z))

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

About:
spreadnatural_numberint_eqtokenatom_eq
inlinrdecideapplyaxiom!abstraction

Definitions MarkB generic Sections NuprlLIB Doc