OAI/Combinatorics/EditApproximation/Specification/ConcreteFootprints.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Concrete allocation traces preserve the cells in the certified Heap construction while keeping its allocation-bound certificates separate.

  1. def OAI.EditApproximation.queryLocalRefinementFootprint line 20
  2. def OAI.EditApproximation.queryLocalRandomSourcesFootprint line 261
  3. def OAI.EditApproximation.queryLocalBandFootprint line 328
  4. def OAI.EditApproximation.queryLocalProgramFootprint line 379
  5. def OAI.EditApproximation.queryPhysicalRandomDataRequestFootprint line 432
  6. def OAI.EditApproximation.queryFamilyRefinementFootprint line 490
  7. def OAI.EditApproximation.queryFamilyActiveFootprint line 516
  8. def OAI.EditApproximation.queryFamilyBoundedActiveFootprint line 536
  9. def OAI.EditApproximation.queryChargedFamilyTableFootprint line 572
  10. def OAI.EditApproximation.queryChargedFamilyGlobalFootprint line 609
  11. def OAI.EditApproximation.queryFamilyMemoRawFootprint line 633
  12. def OAI.EditApproximation.computedQueryMemoRawFootprint line 661
  13. def OAI.EditApproximation.computedQueryMemoFootprint line 679