OAI/Combinatorics/EditApproximation/Binary/BitRankedMemo.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The rank-decreasing evaluator stores the binary words actually returned by its local program. Its rational view preserves the fresh-key, dictionary-visit and request traces.

  1. theorem OAI.EditApproximation.rankedBitMemoEvaluate_decode line 15