OAI/Computability/MatchingCount/BinaryParser.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.BinaryMatching.Parse.RecordBits line 9
  2. def OAI.BinaryMatching.Parse.recordRepr line 10
  3. def OAI.BinaryMatching.Parse.record line 11
  4. lemma OAI.BinaryMatching.Parse.record_encode line 16
  5. lemma OAI.BinaryMatching.Parse.record_size line 20
  6. theorem OAI.BinaryMatching.Parse.record_poly line 27
  7. def OAI.BinaryMatching.Parse.recordStep line 29
  8. lemma OAI.BinaryMatching.Parse.recordStep_nil line 31
  9. lemma OAI.BinaryMatching.Parse.encodeRecord_ne_nil line 35
  10. lemma OAI.BinaryMatching.Parse.recordStep_encode line 37
  11. lemma OAI.BinaryMatching.Parse.recordStep_records line 40
  12. lemma OAI.BinaryMatching.Parse.records_length_le_bits line 47
  13. def OAI.BinaryMatching.Parse.records line 55
  14. lemma OAI.BinaryMatching.Parse.records_encoded line 56
  15. lemma OAI.BinaryMatching.Parse.recordStep_size line 63
  16. lemma OAI.BinaryMatching.Parse.recordStep_iterate_size line 71
  17. theorem OAI.BinaryMatching.Parse.records_poly line 82
  18. def OAI.BinaryMatching.Parse.input line 99
  19. lemma OAI.BinaryMatching.Parse.input_encoded line 102
  20. theorem OAI.BinaryMatching.Parse.input_poly line 105