OAI/Combinatorics/EditApproximation/Queries/QueryLocalSelectors.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The concrete selectors of the adaptive local program. Source and table lookups are evaluated by their counted finite-buffer routines. Their value identities hold even for arbitrary gathered answer lists.

  1. def OAI.EditApproximation.BinaryFraction.queryOnlineSelectWithWork line 22
  2. theorem OAI.EditApproximation.BinaryFraction.queryOnlineSelectWithWork_value line 29
  3. def OAI.EditApproximation.BinaryFraction.queryGroupSelectWithWork line 45
  4. theorem OAI.EditApproximation.BinaryFraction.queryGroupSelectWithWork_value line 51