OAI/Combinatorics/UniformKServer/StackPrimitive.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.UniformKServer.StackPrimitive.Config line 12
  2. def OAI.UniformKServer.StackPrimitive.ofState line 14
  3. def OAI.UniformKServer.StackPrimitive.data line 17
  4. def OAI.UniformKServer.StackPrimitive.apply line 22
  5. def OAI.UniformKServer.StackPrimitive.advance line 26
  6. def OAI.UniformKServer.StackPrimitive.Deterministic line 31
  7. theorem OAI.UniformKServer.StackPrimitive.ofState_step line 34
  8. theorem OAI.UniformKServer.StackPrimitive.apply_primitive line 51
  9. theorem OAI.UniformKServer.StackPrimitive.advance_primitive line 64
  10. theorem OAI.UniformKServer.StackPrimitive.iter_primitive line 80
  11. theorem OAI.UniformKServer.StackPrimitive.ofState_run line 84
  12. theorem OAI.UniformKServer.StackPrimitive.literal_deterministic line 92