OAI/MathematicalPhysics/RapidForcing/FormulaCoding.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.RapidForcing.EffectiveArithmetic.codeUnary line 11
2. lemma OAI.RapidForcing.EffectiveArithmetic.codeUnary_rfind line 12
3. lemma OAI.RapidForcing.EffectiveArithmetic.primrec_codeUnary line 13
4. def OAI.RapidForcing.EffectiveProfile.Formula.toCode line 29
5. def OAI.RapidForcing.EffectiveProfile.Formula.fromCode line 36
6. lemma OAI.RapidForcing.EffectiveProfile.Formula.fromCode_toCode line 44
7. lemma OAI.RapidForcing.EffectiveProfile.Formula.primrec_normalize line 47
8. instance OAI.RapidForcing.EffectiveProfile.Formula.(instance at line 79) line 79
9. lemma OAI.RapidForcing.EffectiveProfile.Formula.encode_toCode line 82
10. lemma OAI.RapidForcing.EffectiveProfile.Formula.primrec_toCode line 84
11. lemma OAI.RapidForcing.EffectiveProfile.Formula.primrec_fromCode line 88
12. lemma OAI.RapidForcing.EffectiveProfile.Formula.primrec_const line 92
13. lemma OAI.RapidForcing.EffectiveProfile.Formula.primrec_var line 97
14. lemma OAI.RapidForcing.EffectiveProfile.Formula.primrec_add line 102
15. lemma OAI.RapidForcing.EffectiveProfile.Formula.primrec_mul line 107
16. lemma OAI.RapidForcing.EffectiveProfile.Formula.primrec_profile line 112
17. lemma OAI.RapidForcing.EffectiveProfile.Formula.computable_recOn line 118