OAI/Combinatorics/EditApproximation/Queries/QueryHistoryBufferCost.lean
3 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.EditApproximation.BinaryFraction.queryEarlierInputsWithWork_timeline 8 - def
OAI.EditApproximation.BinaryFraction.queryEarlierBufferReadBudgetline 19 - theorem
OAI.EditApproximation.BinaryFraction.queryEarlierInputsWithWork_readCostline 22