OAI/Combinatorics/MatchingCount/Tapes/Parse.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatchingFPRAS.LiteralParse.numStep line 10
  2. def OAI.MatchingFPRAS.LiteralParse.eqSymbol line 16
  3. lemma OAI.MatchingFPRAS.LiteralParse.polynomial_eqSymbol line 19
  4. def OAI.MatchingFPRAS.LiteralParse.numStepRealizer line 23
  5. lemma OAI.MatchingFPRAS.LiteralParse.polynomial_numStep line 31
  6. lemma OAI.MatchingFPRAS.LiteralParse.weight_double line 42
  7. lemma OAI.MatchingFPRAS.LiteralParse.weight_double_one line 49
  8. lemma OAI.MatchingFPRAS.LiteralParse.numStep_weight line 54
  9. lemma OAI.MatchingFPRAS.LiteralParse.fold_weight line 73
  10. lemma OAI.MatchingFPRAS.LiteralParse.polynomial_numFold line 82
  11. def OAI.MatchingFPRAS.LiteralParse.parse line 91
  12. def OAI.MatchingFPRAS.LiteralParse.parseRealizer line 92
  13. lemma OAI.MatchingFPRAS.LiteralParse.polynomial_parse line 95
  14. lemma OAI.MatchingFPRAS.LiteralParse.bits_fold line 100
  15. lemma OAI.MatchingFPRAS.LiteralParse.encodeNat_fold line 107
  16. lemma OAI.MatchingFPRAS.LiteralParse.encodeInt_fold line 113
  17. lemma OAI.MatchingFPRAS.LiteralParse.encodeRat_fold line 118