Nuprl Definition : int def

ℤ ==  PRIMITIVE



Rules referencing :  addCommutative addZero addInverse addAssociative multiplyCommutative multiplyOne multiplyAssociative multiplyDistributive addMonotonic lessDiscrete lessTrichotomy intEquality natural_numberEquality minusEquality addEquality multiplyEquality divideEquality remainderEquality divideRemainderSum intWeakElimination int_eqEquality lessEquality baseInt Continuity isintReduceTrue int_eqReduceTrueSq int_eqReduceFalseSq callbyvalueInt callbyvalueAdd callbyvalueMultiply callbyvalueDivide callbyvalueRemainder callbyvalueMinus callbyvalueLess callbyvalueIntEq applyInt exceptionLess exceptionInteq exceptionAdd exceptionMultiply exceptionDivide exceptionRemainder int_eqExceptionCases lessExceptionCases addExceptionCases divideExceptionCases remainderExceptionCases multiplyExceptionCases isintCases lessCases

Latex:
\mBbbZ{}  ==    PRIMITIVE



Date html generated: 2016_05_13-PM-03_03_41
Last ObjectModification: 2006_01_26-PM-03_52_40

Theory : core_1


Home Index