OAI/Combinatorics/EditApproximation/Queries/QueryLocalProgram.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The concrete adaptive local program, beginning with the parent query. Every intermediate buffer is constructed after the answers determining its support, and every scalar source range is computed before its read.

  1. def OAI.EditApproximation.queryLocalProgram line 24
  2. theorem OAI.EditApproximation.queryLocalProgram_refines line 30