OAI/Computability/MatchingCount/SumRoutine.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.BinaryMatching.StackCode.(instance at line 9) line 9
2. instance OAI.BinaryMatching.StackCode.(instance at line 10) line 10
3. theorem OAI.BinaryMatching.StackCode.Poly.some line 16
4. theorem OAI.BinaryMatching.StackCode.Poly.optionToList line 20
5. theorem OAI.BinaryMatching.StackCode.Poly.optionGetD line 23
6. theorem OAI.BinaryMatching.StackCode.Poly.optionIsSome line 27
7. theorem OAI.BinaryMatching.StackCode.Poly.optionMap line 31
8. theorem OAI.BinaryMatching.StackCode.Poly.optionElim line 36
9. theorem OAI.BinaryMatching.StackCode.Poly.sumInl line 41
10. theorem OAI.BinaryMatching.StackCode.Poly.sumInr line 44
11. theorem OAI.BinaryMatching.StackCode.Poly.sumCases line 48