Nuprl Definition : add def
n + m == PRIMITIVE
Rules referencing :
addCommutative,
addZero,
addInverse,
addAssociative,
multiplyDistributive,
addMonotonic,
lessDiscrete,
addEquality,
divideRemainderSum,
intWeakElimination,
bar_Induction,
strong_bar_Induction,
sqlenSubtypeRel,
callbyvalueAdd,
exceptionAdd,
addExceptionCases
Latex:
n + m == PRIMITIVE
Date html generated:
2016_05_13-PM-03_03_44
Last ObjectModification:
2006_01_26-PM-03_53_05
Theory : core_1
Home
Index