OAI/Combinatorics/EditApproximation/Queries/QueryLocalRefinement.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The complete charged local refinement request: earlier history, shared samples, selected current inputs and the final binary continuation.

  1. def OAI.EditApproximation.queryLocalRefinement line 26
  2. theorem OAI.EditApproximation.queryLocalRefinement_refines line 37