OAI/MathematicalPhysics/RapidForcing/NamePrograms.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.RapidForcing.EffectiveProfile.Formula.computable_lipMul line 14
2. lemma OAI.RapidForcing.EffectiveProfile.Formula.computable_lipBound line 27
3. lemma OAI.RapidForcing.EffectiveProfile.Formula.partrec_choosePrecision line 36
4. abbrev OAI.RapidForcing.EffectiveProfile.Formula.NameArgs line 41
5. def OAI.RapidForcing.EffectiveProfile.Formula.nameLip line 42
6. lemma OAI.RapidForcing.EffectiveProfile.Formula.computable_nameLip line 44
7. lemma OAI.RapidForcing.EffectiveProfile.Formula.partrec_evalName line 51
8. lemma OAI.RapidForcing.EffectiveProfile.Formula.partrec_readReal line 69
9. lemma OAI.RapidForcing.EffectiveProfile.Formula.partrec_readPoint line 71
10. lemma OAI.RapidForcing.EffectiveProfile.Formula.partrec_coordinateName line 74
11. def OAI.RapidForcing.EffectiveProfile.Formula.coordinateProgram line 87
12. lemma OAI.RapidForcing.EffectiveProfile.Formula.computable_coordinateProgram line 90
13. lemma OAI.RapidForcing.EffectiveProfile.Formula.runTyped_coordinateProgram line 93