OAI/Combinatorics/EditApproximation/Geometry/RankedMemoProgram.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Well-founded recursive memo evaluation. A local query program may choose later requests from earlier answers. Each recursive request carries its strict rank decrease; no complete table is evaluated in advance.

  1. def OAI.EditApproximation.FiniteQuery.value line 19
  2. theorem OAI.EditApproximation.FiniteQuery.run_sound line 25
  3. def OAI.EditApproximation.FiniteQuery.gather line 44

    Source documentation

    Gather a finite list before running the dependent local continuation.

    def gather {ι : Type*} : List ι → (List ℚ → FiniteQuery ι) → FiniteQuery ι
  | [], next => next []
  | key :: keys, next => .read key (fun result => gather keys (fun results => next (result :: results)))

    Mentions: OAI.EditApproximation.FiniteQuery, OAI.EditApproximation.FiniteQuery.keys

  4. theorem OAI.EditApproximation.FiniteQuery.gather_value line 48
  5. def OAI.EditApproximation.rankedProgramValue line 57
  6. theorem OAI.EditApproximation.memoSound_insert line 65
  7. theorem OAI.EditApproximation.rankedMemoEvaluate_sound line 80
  8. theorem OAI.EditApproximation.rankedMemoEvaluate_empty line 125