OAI/Combinatorics/UniformKServer/ConstructorProgram.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.UniformKServer.ConstructorProgram.read line 13
  2. def OAI.UniformKServer.ConstructorProgram.result line 15
  3. def OAI.UniformKServer.ConstructorProgram.run line 19
  4. theorem OAI.UniformKServer.ConstructorProgram.primitive_read line 22
  5. theorem OAI.UniformKServer.ConstructorProgram.primitive_result line 25
  6. theorem OAI.UniformKServer.ConstructorProgram.run_partrec line 30
  7. def OAI.UniformKServer.ConstructorProgram.code line 36
  8. theorem OAI.UniformKServer.ConstructorProgram.code_correct line 39
  9. theorem OAI.UniformKServer.ConstructorProgram.input_code line 45
  10. theorem OAI.UniformKServer.ConstructorProgram.read_code line 51