Nuprl Definition : int_eq def
In Nuprl the integers are primitive (rather than constructed inductively).
Therefore the basic arithmetic operations are implemented in the computation
system (using LISP bignum package) and axiomatized in the rules.
The operation
if a=b then c else d
is the primitive equality test on integers a and b,
returning c when a=b and d otherwise.
The only rules we need for this are:
int_eqReduceTrueSq which says:
H ⊢ if a=b then s else t ~ u
BY int_eqReduceTrueSq ()
H ⊢ s ~ u
H ⊢ a = b
and
int_eqReduceFalseSq which says:
H ⊢ if a=b then s else t ~ u
BY int_eqReduceFalseSq ()
H ⊢ t ~ u
H ⊢ (a = b) ⟶ Void⋅
if a=b then c else d == PRIMITIVE
Rules referencing :
int_eqEquality,
bar_Induction,
strong_bar_Induction,
SquashedBarInduction,
SquashedBarInductionSqBase,
choiceSequenceRec,
int_eqReduceTrueSq,
int_eqReduceFalseSq,
callbyvalueIntEq,
exceptionInteq,
int_eqExceptionCases
Latex:
if a=b then c else d == PRIMITIVE
Date html generated:
2016_07_08-PM-04_46_26
Last ObjectModification:
2015_10_29-PM-06_18_04
Theory : core_1
Home
Index