OAI/Combinatorics/MatchingCount/Machines/TreeTyped.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. class OAI.MatchingFPRAS.TreeTyped.Codec line 10
2. instance OAI.MatchingFPRAS.TreeTyped.(instance at line 13) line 13
3. instance OAI.MatchingFPRAS.TreeTyped.(instance at line 14) line 14
4. instance OAI.MatchingFPRAS.TreeTyped.(instance at line 15) line 15
5. instance OAI.MatchingFPRAS.TreeTyped.(instance at line 16) line 16
6. instance OAI.MatchingFPRAS.TreeTyped.(instance at line 17) line 17
7. lemma OAI.MatchingFPRAS.TreeTyped.encode_prod line 18
8. lemma OAI.MatchingFPRAS.TreeTyped.encode_list_nil line 20
9. lemma OAI.MatchingFPRAS.TreeTyped.encode_list_cons line 21
10. def OAI.MatchingFPRAS.TreeTyped.Realizes line 24
11. structure OAI.MatchingFPRAS.TreeTyped.Realizer line 26
12. def OAI.MatchingFPRAS.TreeTyped.composition line 33
13. def OAI.MatchingFPRAS.TreeTyped.pair line 36
14. def OAI.MatchingFPRAS.TreeTyped.identity line 55
15. def OAI.MatchingFPRAS.TreeTyped.first line 58
16. def OAI.MatchingFPRAS.TreeTyped.second line 70
17. def OAI.MatchingFPRAS.TreeTyped.add line 80