OAI/Combinatorics/UniformKServer/TypedStack.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.UniformKServer.TypedStack.Action line 12
  2. structure OAI.UniformKServer.TypedStack.Processor line 18
  3. structure OAI.UniformKServer.TypedStack.State line 21
  4. def OAI.UniformKServer.TypedStack.step line 30
  5. def OAI.UniformKServer.TypedStack.initial line 35
  6. def OAI.UniformKServer.TypedStack.install line 37
  7. def OAI.UniformKServer.TypedStack.run line 39
  8. def OAI.UniformKServer.TypedStack.eqv line 42
  9. def OAI.UniformKServer.TypedStack.compile line 44
  10. def OAI.UniformKServer.TypedStack.encode line 50
  11. theorem OAI.UniformKServer.TypedStack.encode_step line 54
  12. theorem OAI.UniformKServer.TypedStack.encode_run line 60
  13. theorem OAI.UniformKServer.TypedStack.encode_initial line 68
  14. theorem OAI.UniformKServer.TypedStack.encode_install line 71
  15. theorem OAI.UniformKServer.TypedStack.run_cons line 74
  16. theorem OAI.UniformKServer.TypedStack.run_append line 77
  17. theorem OAI.UniformKServer.TypedStack.run_yielded line 80