OAI/Combinatorics/MatchingCount/Tapes/Codec.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatchingFPRAS.TreeTyped.Realizer.reencode line 8
  2. lemma OAI.MatchingFPRAS.TreeTyped.polynomial_reencode line 17
  3. def OAI.MatchingFPRAS.LiteralCodec.parts line 29
  4. instance OAI.MatchingFPRAS.LiteralCodec.(instance at line 31) line 31
  5. lemma OAI.MatchingFPRAS.LiteralCodec.encode_parts line 32
  6. lemma OAI.MatchingFPRAS.LiteralCodec.weight_false_list line 33
  7. lemma OAI.MatchingFPRAS.LiteralCodec.weight_symbol line 37
  8. lemma OAI.MatchingFPRAS.LiteralCodec.weight_word line 42
  9. def OAI.MatchingFPRAS.LiteralCodec.valRealizer line 47
  10. lemma OAI.MatchingFPRAS.LiteralCodec.polynomial_val line 49
  11. def OAI.MatchingFPRAS.LiteralCodec.fromBit line 52
  12. def OAI.MatchingFPRAS.LiteralCodec.fromBitRealizer line 53
  13. lemma OAI.MatchingFPRAS.LiteralCodec.polynomial_fromBit line 54
  14. def OAI.MatchingFPRAS.LiteralCodec.natWord line 56
  15. def OAI.MatchingFPRAS.LiteralCodec.natWordRealizer line 57
  16. lemma OAI.MatchingFPRAS.LiteralCodec.polynomial_natWord line 59
  17. lemma OAI.MatchingFPRAS.LiteralCodec.natWord_eq line 66
  18. def OAI.MatchingFPRAS.LiteralCodec.ratWord line 68
  19. def OAI.MatchingFPRAS.LiteralCodec.ratWordRealizer line 69
  20. lemma OAI.MatchingFPRAS.LiteralCodec.polynomial_ratWord line 72
  21. lemma OAI.MatchingFPRAS.LiteralCodec.ratWord_repr line 77