OAI/Combinatorics/EditApproximation/Coarse/CoarseReadBudget.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.EditApproximation.CoarseReadBudget line 9

   Source documentation

   A finite uniform bound on the actually executed source-index operations. The depth and offset ranges are the original padded source capacity.

   structure CoarseReadBudget (B R k n : ℕ) (source target : List ℕ) (K : ℕ) : Prop where
   …

2. theorem OAI.EditApproximation.coarseReadBudget_height line 20