OAI/Combinatorics/EditApproximation/Geometry/MemoizedOracle.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Persistent dictionary requests. A fresh oracle is called only on a cache miss; subsequent requests preserve and return the stored answer.

  1. structure OAI.EditApproximation.MemoRequestResult line 10
  2. def OAI.EditApproximation.memoRequest line 20
  3. theorem OAI.EditApproximation.memoRequest_lookup line 29
  4. theorem OAI.EditApproximation.memoRequest_preserves line 35
  5. theorem OAI.EditApproximation.memoRequest_fresh_iff line 48
  6. theorem OAI.EditApproximation.memoRequest_visits line 54
  7. def OAI.EditApproximation.memoSound line 63
  8. theorem OAI.EditApproximation.memoRequest_sound line 66
  9. structure OAI.EditApproximation.MemoBatchResult line 86
  10. def OAI.EditApproximation.memoRequests line 92
  11. theorem OAI.EditApproximation.memoRequests_preserves line 101
  12. theorem OAI.EditApproximation.memoRequests_fresh_absent line 109
  13. theorem OAI.EditApproximation.memoRequests_fresh_nodup line 130
  14. theorem OAI.EditApproximation.memoRequests_fresh_subset line 146
  15. theorem OAI.EditApproximation.memoRequests_fresh_count line 159
  16. theorem OAI.EditApproximation.memoRequests_visits line 167
  17. theorem OAI.EditApproximation.memoSound_empty line 177
  18. theorem OAI.EditApproximation.memoRequests_sound line 182