canUseCache — Mathlib

Lean4
/-- We use a cache entry iff the upcoming traversal would abstract exactly the same occurrences
as the cached traversal. -/
def canUseCache (cacheOcc dCacheOcc currOcc : Nat) : Occurrences → Bool
  | .all => true
  | .pos l | .neg l =>
    Id.run
      (do
        let mut prevOccs := #[]
        let mut currOccs := #[]
        for p in l.toArray.qsort do
          if cacheOcc ≤ p && p < cacheOcc + dCacheOcc then
            prevOccs := prevOccs.push (p - cacheOcc)
          if currOcc ≤ p && p < currOcc + dCacheOcc then
            currOccs := currOccs.push (p - currOcc)
        return prevOccs == currOccs)
Похожие утверждения