OAI/Combinatorics/IndependentSets/Encoding/BitsValue.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LargeIndependentSets.BinaryParser.bitsValue line 9
  2. lemma OAI.LargeIndependentSets.BinaryParser.bitsValue_bits line 13
  3. def OAI.LargeIndependentSets.BinaryParser.parseFrame line 18
  4. lemma OAI.LargeIndependentSets.BinaryParser.parseFrame_encoded line 25
  5. def OAI.LargeIndependentSets.BinaryParser.parseName line 31
  6. lemma OAI.LargeIndependentSets.BinaryParser.parseName_encoded line 36
  7. def OAI.LargeIndependentSets.BinaryParser.parseLiteral line 40
  8. lemma OAI.LargeIndependentSets.BinaryParser.parseLiteral_encoded line 46
  9. def OAI.LargeIndependentSets.BinaryParser.parseMany line 51
  10. lemma OAI.LargeIndependentSets.BinaryParser.parseMany_encoded line 59
  11. def OAI.LargeIndependentSets.BinaryParser.parseClause line 72
  12. lemma OAI.LargeIndependentSets.BinaryParser.parseClause_encoded line 76
  13. lemma OAI.LargeIndependentSets.BinaryParser.clauses_length_le_bits line 82
  14. def OAI.LargeIndependentSets.BinaryParser.core line 94
  15. lemma OAI.LargeIndependentSets.BinaryParser.core_encoded line 103
  16. def OAI.LargeIndependentSets.BinaryParser.decode line 114
  17. theorem OAI.LargeIndependentSets.BinaryParser.decode_encoded line 119
  18. theorem OAI.LargeIndependentSets.BinaryParser.decode_bits_bound line 122