Definitions MarkB generic Sections NuprlLIB Doc

No other cites to report in MarkB_generic
case_enum1_el1Def enum1_el1 = > body cont(x,z) == InjCase(if x=0 inl(*) ; inr(*) fi ; body; cont(z,z))

Syntax:enum1_el1 = > body cont has structure: case_enum1_el1(body; cont)

About:
natural_numberint_eqinlinr
decideapplyaxiom
!abstraction

Definitions MarkB generic Sections NuprlLIB Doc