OAI/Combinatorics/UniformKServer/RawProgram.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.UniformKServer.RawProgram.Payload line 15
  2. def OAI.UniformKServer.RawProgram.payload line 17
  3. def OAI.UniformKServer.RawProgram.initial line 18
  4. def OAI.UniformKServer.RawProgram.unpack line 19
  5. def OAI.UniformKServer.RawProgram.request line 21
  6. def OAI.UniformKServer.RawProgram.fresh line 23
  7. def OAI.UniformKServer.RawProgram.chosen line 26
  8. def OAI.UniformKServer.RawProgram.next line 30
  9. def OAI.UniformKServer.RawProgram.randomCount line 35
  10. def OAI.UniformKServer.RawProgram.run line 37
  11. theorem OAI.UniformKServer.RawProgram.primitive_natCode line 44
  12. theorem OAI.UniformKServer.RawProgram.primitive_unpack line 55
  13. theorem OAI.UniformKServer.RawProgram.primitive_request line 58
  14. theorem OAI.UniformKServer.RawProgram.primitive_fresh line 60
  15. theorem OAI.UniformKServer.RawProgram.primitive_chosen line 67
  16. theorem OAI.UniformKServer.RawProgram.primitive_next line 70
  17. theorem OAI.UniformKServer.RawProgram.primitive_randomCount line 73
  18. theorem OAI.UniformKServer.RawProgram.primitive_get line 75
  19. theorem OAI.UniformKServer.RawProgram.primitive_run line 77
  20. theorem OAI.UniformKServer.RawProgram.unpack_encode line 85
  21. theorem OAI.UniformKServer.RawProgram.request_code line 87