OAI/Computability/MatchingCount/RecursiveCoding.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BinaryMatching.RecursiveEval.branchRepr line 10
  2. def OAI.BinaryMatching.RecursiveEval.commandRepr line 13
  3. instance OAI.BinaryMatching.RecursiveEval.(instance at line 16) line 16
  4. instance OAI.BinaryMatching.RecursiveEval.(instance at line 17) line 17
  5. instance OAI.BinaryMatching.RecursiveEval.(instance at line 18) line 18
  6. theorem OAI.BinaryMatching.RecursiveEval.Compile.leaf_poly line 23
  7. theorem OAI.BinaryMatching.RecursiveEval.Compile.fork_poly line 25
  8. theorem OAI.BinaryMatching.RecursiveEval.Compile.call_poly line 27
  9. theorem OAI.BinaryMatching.RecursiveEval.Compile.join_poly line 29
  10. theorem OAI.BinaryMatching.RecursiveEval.Compile.branchCasesWith line 32
  11. theorem OAI.BinaryMatching.RecursiveEval.Compile.commandCasesWith line 46