OAI/Computability/Scheduling/Parser.lean

GitHub source file

60 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ThreeMachine.StackCompiler.Binary.value line 11
  2. def OAI.ThreeMachine.StackCompiler.Binary.increment line 15
  3. def OAI.ThreeMachine.StackCompiler.Binary.leading line 20
  4. theorem OAI.ThreeMachine.StackCompiler.Binary.leading_nil line 22
  5. theorem OAI.ThreeMachine.StackCompiler.Binary.leading_false line 23
  6. theorem OAI.ThreeMachine.StackCompiler.Binary.leading_true line 24
  7. theorem OAI.ThreeMachine.StackCompiler.Binary.increment_formula line 27
  8. theorem OAI.ThreeMachine.StackCompiler.Binary.increment_encodePosNum line 37
  9. theorem OAI.ThreeMachine.StackCompiler.Binary.increment_encodeNum line 44
  10. theorem OAI.ThreeMachine.StackCompiler.Binary.increment_encodeNat line 50
  11. theorem OAI.ThreeMachine.StackCompiler.Binary.iterate_increment line 58
  12. theorem OAI.ThreeMachine.StackCompiler.Binary.value_encodePosNum line 63
  13. theorem OAI.ThreeMachine.StackCompiler.Binary.value_encodeNat line 69
  14. def OAI.ThreeMachine.StackCompiler.Binary.leadingStep line 76
  15. theorem OAI.ThreeMachine.StackCompiler.Binary.leading_fold line 79
  16. def OAI.ThreeMachine.StackCompiler.Binary.takeStep line 95
  17. theorem OAI.ThreeMachine.StackCompiler.Binary.takeStep_iterate line 98
  18. def OAI.ThreeMachine.StackCompiler.Binary.valueStep line 109
  19. theorem OAI.ThreeMachine.StackCompiler.Binary.value_fold line 111
  20. def OAI.ThreeMachine.StackCompiler.Binary.readNat line 120
  21. theorem OAI.ThreeMachine.StackCompiler.Binary.leading_encodeNat line 125
  22. theorem OAI.ThreeMachine.StackCompiler.Binary.readNat_encodeNat line 133
  23. def OAI.ThreeMachine.StackCompiler.Uniform.replicate line 150
  24. def OAI.ThreeMachine.StackCompiler.Uniform.binaryLeadingStep line 154
  25. def OAI.ThreeMachine.StackCompiler.Uniform.binaryLeading line 159
  26. def OAI.ThreeMachine.StackCompiler.Uniform.takeStep line 163
  27. def OAI.ThreeMachine.StackCompiler.Uniform.take line 168
  28. def OAI.ThreeMachine.StackCompiler.Uniform.binaryValueStep line 172
  29. def OAI.ThreeMachine.StackCompiler.Uniform.binaryValue line 177
  30. def OAI.ThreeMachine.StackCompiler.Uniform.binaryReadNat line 180
  31. def OAI.ThreeMachine.StackCompiler.Uniform.binaryIncrement line 187
  32. def OAI.ThreeMachine.StackCompiler.Uniform.rawEncodeNat line 195
  33. def OAI.ThreeMachine.StackCompiler.Uniform.binaryEncodeNat line 198
  34. def OAI.ThreeMachine.StackCompiler.Uniform.binaryEncodeList line 202
  35. def OAI.ThreeMachine.StackCompiler.Uniform.binaryEncodeAnswer line 206
  36. def OAI.ThreeMachine.StackCompiler.Binary.readStep line 217
  37. def OAI.ThreeMachine.StackCompiler.Binary.readMany line 221
  38. theorem OAI.ThreeMachine.StackCompiler.Binary.readStep_iterate line 225
  39. theorem OAI.ThreeMachine.StackCompiler.Binary.readMany_correct line 236
  40. def OAI.ThreeMachine.StackCompiler.Binary.readList line 241
  41. theorem OAI.ThreeMachine.StackCompiler.Binary.readList_correct line 245
  42. def OAI.ThreeMachine.StackCompiler.Binary.encodeEdge line 251
  43. def OAI.ThreeMachine.StackCompiler.Binary.readEdge line 253
  44. theorem OAI.ThreeMachine.StackCompiler.Binary.readEdge_correct line 258
  45. def OAI.ThreeMachine.StackCompiler.Binary.readHeader line 262
  46. def OAI.ThreeMachine.StackCompiler.Binary.encodeHeader line 268
  47. theorem OAI.ThreeMachine.StackCompiler.Binary.readHeader_correct line 272
  48. def OAI.ThreeMachine.StackCompiler.Binary.parse line 280
  49. theorem OAI.ThreeMachine.StackCompiler.Binary.encodeEdges_map line 286
  50. theorem OAI.ThreeMachine.StackCompiler.Binary.parse_input line 292
  51. def OAI.ThreeMachine.StackCompiler.Uniform.binaryReadStep line 309
  52. def OAI.ThreeMachine.StackCompiler.Uniform.binaryReadMany line 314
  53. def OAI.ThreeMachine.StackCompiler.Uniform.binaryReadList line 319
  54. def OAI.ThreeMachine.StackCompiler.Uniform.binaryReadEdge line 323
  55. def OAI.ThreeMachine.StackCompiler.Uniform.binaryReadHeader line 329
  56. def OAI.ThreeMachine.StackCompiler.Uniform.binaryParse line 335
  57. structure OAI.ThreeMachine.StackCompiler.Request line 345
  58. instance OAI.ThreeMachine.StackCompiler.(instance at line 349) line 349
  59. def OAI.ThreeMachine.StackCompiler.Uniform.parseRequest line 354
  60. def OAI.ThreeMachine.StackCompiler.Uniform.requestAnswer line 366