fix: account for lean4#3851 (#123)

Co-authored-by: Scott Morrison <[email protected]>

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 =>

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