chore: use Array.findFinIdx? where it is better than findIdx?

src/Init/Data/ByteArray/Basic.lean

@@ -108,8 +108,18 @@ def toList (bs : ByteArray) : List UInt8 :=
 
 @[inline] def findIdx? (a : ByteArray) (p : UInt8 → Bool) (start := 0) : Option Nat :=
   let rec @[specialize] loop (i : Nat) :=
-    if i < a.size then
-      if p (a.get! i) then some i else loop (i+1)
+    if h : i < a.size then
+      if p a[i] then some i else loop (i+1)
+    else
+      none
+    termination_by a.size - i
+    decreasing_by decreasing_trivial_pre_omega
+  loop start
+
+@[inline] def findFinIdx? (a : ByteArray) (p : UInt8 → Bool) (start := 0) : Option (Fin a.size) :=
+  let rec @[specialize] loop (i : Nat) :=
+    if h : i < a.size then
+      if p a[i] then some ⟨i, h⟩ else loop (i+1)
     else
       none
     termination_by a.size - i

src/Lean/Compiler/LCNF/PassManager.lean

@@ -157,9 +157,7 @@ def installBeforeEachOccurrence (targetName : Name) (p : Pass → Pass) : PassIn
 def replacePass (targetName : Name) (p : Pass → Pass) (occurrence : Nat := 0) : PassInstaller where
   install passes := do
     let some idx := passes.findIdx? (fun p => p.name == targetName && p.occurrence == occurrence) | throwError s!"Tried to replace {targetName}, occurrence {occurrence} but {targetName} is not in the pass list"
-    let target := passes[idx]!
-    let replacement := p target
-    return passes.set! idx replacement
+    return passes.modify idx p
 
 def replaceEachOccurrence (targetName : Name) (p : Pass → Pass) : PassInstaller :=
     withEachOccurrence targetName (replacePass targetName p ·)

src/Lean/Elab/Notation.lean

@@ -17,7 +17,7 @@ open Lean.Parser.Command
 private partial def antiquote (vars : Array Syntax) : Syntax → Syntax
   | stx => match stx with
   | `($id:ident) =>
-    if (vars.findIdx? (fun var => var.getId == id.getId)).isSome then
+    if vars.any (fun var => var.getId == id.getId) then
       mkAntiquotNode id (kind := `term) (isPseudoKind := true)
     else
       stx

src/Lean/Elab/PreDefinition/Structural/BRecOn.lean

@@ -145,8 +145,8 @@ private partial def replaceRecApps (recArgInfos : Array RecArgInfo) (positions :
     | Expr.app _ _ =>
       let processApp (e : Expr) : StateRefT (HasConstCache recFnNames) M Expr :=
         e.withApp fun f args => do
-          if let .some fnIdx := recArgInfos.findIdx? (f.isConstOf ·.fnName) then
-            let recArgInfo := recArgInfos[fnIdx]!
+          if let .some fnIdx := recArgInfos.findFinIdx? (f.isConstOf ·.fnName) then
+            let recArgInfo := recArgInfos[fnIdx]
             let some recArg := args[recArgInfo.recArgPos]?
               | throwError "insufficient number of parameters at recursive application {indentExpr e}"
             -- For reflexive type, we may have nested recursive applications in recArg

src/Lean/Meta/IndPredBelow.lean

@@ -152,7 +152,7 @@ where
     let run (x : StateRefT Nat MetaM Expr) : MetaM (Expr × Nat) := StateRefT'.run x 0
     let (_, cnt) ← run <| transform domain fun e => do
       if let some name := e.constName? then
-        if let some _ := ctx.typeInfos.findIdx? fun indVal => indVal.name == name then
+        if ctx.typeInfos.any fun indVal => indVal.name == name then
           modify (· + 1)
       return .continue
 

src/Std/Time/Zoned/ZoneRules.lean

@@ -147,9 +147,7 @@ If the timestamp falls between two transitions, it returns the most recent trans
 -/
 def findTransitionIndexForTimestamp (transitions : Array Transition) (timestamp : Timestamp) : Option Nat :=
   let value := timestamp.toSecondsSinceUnixEpoch
-  if let some idx := transitions.findIdx? (fun t => t.time.val > value.val)
-    then some idx
-    else none
+  transitions.findIdx? (fun t => t.time.val > value.val)
 
 /--
 Finds the transition corresponding to a given timestamp in `Array Transition`.

src/Std/Time/Zoned/ZonedDateTime.lean

@@ -61,16 +61,16 @@ def ofPlainDateTime (pdt : PlainDateTime) (zr : TimeZone.ZoneRules) : ZonedDateT
 
   let transition :=
     let value := tm.toSecondsSinceUnixEpoch
-    if let some idx := zr.transitions.findIdx? (fun t => t.time.val ≥ value.val)
-      then do
-        let last ← zr.transitions.get? (idx - 1)
-        let next ← zr.transitions.get? idx <|> zr.transitions.back?
+    if let some idx := zr.transitions.findFinIdx? (fun t => t.time.val ≥ value.val)
+      then
+        let last := zr.transitions[idx.1 - 1]
+        let next := zr.transitions[idx]
 
         let utcNext := next.time.sub last.localTimeType.gmtOffset.second.abs
 
         if utcNext.val > tm.toSecondsSinceUnixEpoch.val
-          then pure last
-          else pure next
+          then some last
+          else some next
 
       else zr.transitions.back?