OAI/Computability/MatchingCount/RawBitsBridge.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.BinaryMatching.StackCode.Bits line 10
  2. instance OAI.BinaryMatching.StackCode.(instance at line 13) line 13
  3. lemma OAI.BinaryMatching.StackCode.encode_Bits line 14
  4. def OAI.BinaryMatching.StackCode.Routine.headBool line 17
  5. theorem OAI.BinaryMatching.StackCode.Poly.bitsTail line 50
  6. theorem OAI.BinaryMatching.StackCode.Poly.bitsEmpty line 52
  7. theorem OAI.BinaryMatching.StackCode.Poly.bitsHead line 54
  8. theorem OAI.BinaryMatching.StackCode.Poly.bitsLength line 56
  9. theorem OAI.BinaryMatching.StackCode.Poly.bitsAppend line 57
  10. theorem OAI.BinaryMatching.StackCode.Poly.bitsSingleton line 59
  11. def OAI.BinaryMatching.StackCode.encodeBitsStep line 63
  12. lemma OAI.BinaryMatching.StackCode.encodeBitsStep_iterate line 65
  13. theorem OAI.BinaryMatching.StackCode.Poly.bitsDecode line 76
  14. lemma OAI.BinaryMatching.StackCode.Poly.bits_fold line 93
  15. theorem OAI.BinaryMatching.StackCode.Poly.bitsEncode line 99