OAI/Combinatorics/EditApproximation/Queries/QueryLocalFinishCost.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The executed refinement tail, with its actual selected actions and its final deduplicated current-input buffer.

  1. def OAI.EditApproximation.BinaryFraction.queryFinishReadBudget line 12
  2. theorem OAI.EditApproximation.BinaryFraction.queryLocalRefinement_finish_bounds line 29