OAI/Combinatorics/EditDistance/BinaryCode.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Binary delimiter codes and padding

  1. def OAI.EditCode.width line 13
  2. def OAI.EditCode.bit line 15
  3. def OAI.EditCode.block line 19
  4. def OAI.EditCode.encode line 22
  5. def OAI.EditCode.padded line 24
  6. lemma OAI.EditCode.block_length line 27
  7. lemma OAI.EditCode.width_pos line 30
  8. lemma OAI.EditCode.encode_length line 32
  9. lemma OAI.EditCode.padded_length line 38
  10. lemma OAI.EditCode.bit_zero line 41
  11. lemma OAI.EditCode.bit_one line 42
  12. lemma OAI.EditCode.bit_label line 44
  13. lemma OAI.EditCode.bit_even line 50
  14. lemma OAI.EditCode.bit_last line 54
  15. lemma OAI.EditCode.bit_consecutive line 60
  16. lemma OAI.EditCode.encode_get_block line 71
  17. lemma OAI.EditCode.padded_get_block line 99
  18. lemma OAI.EditCode.padded_get_padding line 115
  19. lemma OAI.EditCode.padded_delimiter line 122
  20. lemma OAI.EditCode.block_injective line 157