Nuprl Definition : natural_number def
$n == PRIMITIVE
Rules referencing :
addZero,
addInverse,
multiplyOne,
lessDiscrete,
multiplyPositive,
natural_numberEquality,
divideEquality,
remainderEquality,
remainderBounds1,
remainderBounds2,
remainderBounds3,
remainderBounds4,
divideRemainderSum,
intWeakElimination,
bar_Induction,
strong_bar_Induction,
StrongContinuity2,
sqlenSubtypeRel,
sqequalZero,
sqleZero,
callbyvalueReduce,
callbyvalueInt,
callbyvalueAtom1,
callbyvalueAtom2,
callbyvalueAtom,
callbyvalueType,
callbyvalueAdd,
callbyvalueMultiply,
callbyvalueDivide,
callbyvalueRemainder,
callbyvalueMinus,
callbyvalueLess,
callbyvalueIntEq,
callbyvalueAtomEq,
callbyvalueAtomnEq,
callbyvalueApply,
tryReduceValue,
callbyvalueCallbyvalue,
callbyvalueSpread,
callbyvalueDecide,
callbyvalueIspair,
callbyvalueIsaxiom,
callbyvalueIsinl,
callbyvalueIsinr,
callbyvalueIslambda,
callbyvalueIsint,
callbyvalueIsatom,
callbyvalueIsatom1,
callbyvalueIsatom2,
ispairCases,
isintCases,
isatomCases,
isaxiomCases,
islambdaCases,
isinlCases,
isinrCases,
isatom1Cases,
isatom2Cases
Latex:
\$n == PRIMITIVE
Date html generated:
2016_05_13-PM-03_03_42
Last ObjectModification:
2006_01_26-PM-03_52_47
Theory : core_1
Home
Index