From decc71a7d3da55585b47658b9b74d4572a5d5169 Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Sun, 14 Apr 2024 22:56:15 -0700 Subject: [PATCH] fix: account for lean4#3851 (#123) Co-authored-by: Scott Morrison --- Aesop/Search/Expansion.lean | 2 +- Aesop/Util/Basic.lean | 16 ---------------- 2 files changed, 1 insertion(+), 17 deletions(-) diff --git a/Aesop/Search/Expansion.lean b/Aesop/Search/Expansion.lean index 502e1562..aef08f55 100644 --- a/Aesop/Search/Expansion.lean +++ b/Aesop/Search/Expansion.lean @@ -207,7 +207,7 @@ partial def runFirstUnsafeRule (postponedSafeRules : Array PostponedSafeRule) return result where loop (queue : UnsafeQueue) : SearchM Q (UnsafeQueue × RuleResult) := do - let (some (r, queue)) := Subarray.popFront? queue + let (some (r, queue)) := Subarray.popHead? queue | return (queue, RuleResult.failed) match r with | .unsafeRule r => diff --git a/Aesop/Util/Basic.lean b/Aesop/Util/Basic.lean index 7732e725..65f7038e 100644 --- a/Aesop/Util/Basic.lean +++ b/Aesop/Util/Basic.lean @@ -25,22 +25,6 @@ theorem size_modify (a : Array α) (i : Nat) (f : α → α) : end Array -namespace Subarray - -def popFront? (as : Subarray α) : Option (α × Subarray α) := - if h : as.start < as.stop - then - let head := as.as.get ⟨as.start, Nat.lt_of_lt_of_le h as.h₂⟩ - let tail := - { as with - start := as.start + 1 - h₁ := Nat.le_of_lt_succ $ Nat.succ_lt_succ h } - some (head, tail) - else - none - -end Subarray - @[inline] def time [Monad m] [MonadLiftT BaseIO m] (x : m α) : m (α × Aesop.Nanos) := do let start ← IO.monoNanosNow