OAI/MathematicalPhysics/RapidForcing/ExprCoding.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RapidForcing.EffectiveArithmetic.primrec_code_pair line 11
  2. lemma OAI.RapidForcing.EffectiveArithmetic.primrec_code_comp line 13
  3. lemma OAI.RapidForcing.EffectiveArithmetic.primrec_code_prec line 15
  4. lemma OAI.RapidForcing.EffectiveArithmetic.primrec_code_ofNat line 18
  5. def OAI.RapidForcing.EffectiveArithmetic.retractEncodable line 20
  6. def OAI.RapidForcing.EffectiveArithmetic.primcodable_retract line 23
  7. lemma OAI.RapidForcing.EffectiveArithmetic.code_encode_ofNat line 37
  8. def OAI.RapidForcing.EffectiveProfile.Expr.toCode line 48
  9. def OAI.RapidForcing.EffectiveProfile.Expr.fromCode line 56
  10. lemma OAI.RapidForcing.EffectiveProfile.Expr.fromCode_toCode line 65
  11. lemma OAI.RapidForcing.EffectiveProfile.Expr.primrec_normalize line 68
  12. instance OAI.RapidForcing.EffectiveProfile.Expr.(instance at line 99) line 99
  13. lemma OAI.RapidForcing.EffectiveProfile.Expr.primrec_toCode line 101
  14. lemma OAI.RapidForcing.EffectiveProfile.Expr.primrec_fromCode line 105
  15. lemma OAI.RapidForcing.EffectiveProfile.Expr.encode_toCode line 109
  16. lemma OAI.RapidForcing.EffectiveProfile.Expr.primrec_const line 111
  17. lemma OAI.RapidForcing.EffectiveProfile.Expr.primrec_left line 116
  18. lemma OAI.RapidForcing.EffectiveProfile.Expr.primrec_right line 121
  19. lemma OAI.RapidForcing.EffectiveProfile.Expr.primrec_invDen line 126
  20. lemma OAI.RapidForcing.EffectiveProfile.Expr.primrec_add line 131
  21. lemma OAI.RapidForcing.EffectiveProfile.Expr.primrec_mul line 136