OAI/Combinatorics/EditApproximation/Binary/BitQuerySpace.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Allocation annotations for the actual adaptive query. Charge annotations carry the concrete routine's allocation bound; reads reserve three cells for its suspended continuation and result pointer. Charge transitions are tail transitions. Summing all allocations bounds simultaneously live cells even if no temporary cell is reclaimed until the query returns.

  1. inductive OAI.EditApproximation.BitQuery.Heap line 13
  2. def OAI.EditApproximation.BitQuery.Heap.cells line 22
  3. theorem OAI.EditApproximation.BitQuery.Heap.cells_le_work line 27
  4. def OAI.EditApproximation.BitQuery.Heap.bind line 39
  5. def OAI.EditApproximation.BitQuery.Heap.compute line 46
  6. def OAI.EditApproximation.BitQuery.Heap.chargeOf line 50
  7. def OAI.EditApproximation.BitQuery.Heap.computeOf line 54
  8. def OAI.EditApproximation.BitQuery.Heap.collect line 58