OAI/MathematicalPhysics/RapidForcing/IntegerPrimrec.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.RapidForcing.EffectiveArithmetic.encode_int_ofNat line 11
2. lemma OAI.RapidForcing.EffectiveArithmetic.encode_int_negSucc line 17
3. lemma OAI.RapidForcing.EffectiveArithmetic.ofNat_int line 21
4. lemma OAI.RapidForcing.EffectiveArithmetic.primrec_int_ofNat line 31
5. lemma OAI.RapidForcing.EffectiveArithmetic.primrec_int_negSucc line 35
6. lemma OAI.RapidForcing.EffectiveArithmetic.primrec_int_cases line 40
7. lemma OAI.RapidForcing.EffectiveArithmetic.primrec_int_natAbs line 56
8. lemma OAI.RapidForcing.EffectiveArithmetic.primrec_int_toNat line 60
9. lemma OAI.RapidForcing.EffectiveArithmetic.primrec_int_neg line 64