OAI/Combinatorics/UniformKServer/RawBinary.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.UniformKServer.RawBinary.value line 14
  2. theorem OAI.UniformKServer.RawBinary.value_nil line 16
  3. theorem OAI.UniformKServer.RawBinary.value_cons line 17
  4. theorem OAI.UniformKServer.RawBinary.value_bits line 20
  5. theorem OAI.UniformKServer.RawBinary.primitive_value line 25
  6. def OAI.UniformKServer.RawBinary.readNat line 36
  7. theorem OAI.UniformKServer.RawBinary.read_natCode line 41
  8. def OAI.UniformKServer.RawBinary.readQ line 51
  9. theorem OAI.UniformKServer.RawBinary.read_rationalCode line 56
  10. def OAI.UniformKServer.RawBinary.readMany line 61
  11. def OAI.UniformKServer.RawBinary.input line 64
  12. theorem OAI.UniformKServer.RawBinary.primitive_readNat line 71
  13. theorem OAI.UniformKServer.RawBinary.primitive_readQ line 79
  14. theorem OAI.UniformKServer.RawBinary.primitive_readMany line 81
  15. theorem OAI.UniformKServer.RawBinary.primitive_input line 87
  16. theorem OAI.UniformKServer.RawBinary.fold_read line 91
  17. theorem OAI.UniformKServer.RawBinary.readMany_codes line 102
  18. def OAI.UniformKServer.RawBinary.distances line 106
  19. theorem OAI.UniformKServer.RawBinary.distances_length line 109
  20. theorem OAI.UniformKServer.RawBinary.distance_codes line 112
  21. theorem OAI.UniformKServer.RawBinary.input_code line 120
  22. theorem OAI.UniformKServer.RawBinary.distances_ofFn line 126
  23. theorem OAI.UniformKServer.RawBinary.metric_input line 141