IndisputableMonolith.Foundation.IntegersFromLogic

declarations in this module (42)

• def intRel L42
• theorem intRel_refl L45
• theorem intRel_symm L50
• theorem intRel_trans L55
• instance setoid L70
• def LogicInt L77
• def mk L82
• theorem sound L88
• def ofLogicNat L98
• theorem ofLogicNat_zero L100
• def zero L105
• def one L108
• def neg L114
• def add L129
• def mul L149
• def toIntCore L180
• theorem toIntCore_respects L183
• def toInt L196
• def fromInt L200
• theorem toInt_mk L204
• theorem toInt_fromInt L207
• theorem fromInt_toInt L219
• def equivInt L300
• theorem toInt_zero L313
• theorem toInt_one L318
• theorem toInt_add L323
• theorem toInt_neg L336
• theorem toInt_mul L344
• theorem eq_iff_toInt_eq L360
• theorem add_assoc' L373
• theorem add_comm' L376
• theorem zero_add' L379
• theorem add_zero' L382
• theorem add_left_neg' L385
• theorem mul_assoc' L388
• theorem mul_comm' L391
• theorem one_mul' L394
• theorem mul_one' L397
• theorem mul_add' L400
• theorem add_mul' L403
• theorem mul_eq_zero L408
• theorem mul_right_cancel L425