OAI/Computability/MinUncut/Search/UniformFiniteSum.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MinUncut.Preprocess.UEncoding.computable_sum line 12
2. def OAI.MinUncut.Preprocess.decodeGood line 25
3. instance OAI.MinUncut.Preprocess.(instance at line 28) line 28
4. lemma OAI.MinUncut.Preprocess.c_searchProj line 33
5. lemma OAI.MinUncut.Preprocess.c_searchEval line 35
6. lemma OAI.MinUncut.Preprocess.c_searchDecode line 42
7. lemma OAI.MinUncut.Preprocess.c_searchBool line 44
8. lemma OAI.MinUncut.Preprocess.searchBool_eq line 50
9. lemma OAI.MinUncut.Preprocess.computable_decodeGood line 53
10. instance OAI.MinUncut.Preprocess.option_elim_decidable line 59
11. lemma OAI.MinUncut.Preprocess.choose_getD line 63
12. def OAI.MinUncut.Preprocess.search line 83
13. lemma OAI.MinUncut.Preprocess.search_spec line 87
14. lemma OAI.MinUncut.Preprocess.computable_search line 91
15. def OAI.MinUncut.Preprocess.searchWith line 104
16. lemma OAI.MinUncut.Preprocess.computable_searchWith line 107