OAI/Combinatorics/EditApproximation/Refinement/PhysicalFamilyProgram.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The actual scalar family supplies the body-value and source-read bounds required by the mixed source/table dependency analysis.

  1. def OAI.EditApproximation.physicalFamilyRequestValue line 27
  2. theorem OAI.EditApproximation.physicalFamilyProgram_value line 34
  3. theorem OAI.EditApproximation.computed_physicalFamilyProgram_source_cost line 63