finish

src/Init/Data/Array/Basic.lean

@@ -656,18 +656,30 @@ def findFinIdx? {α : Type u} (p : α → Bool) (as : Array α) : Option (Fin as
     decreasing_by simp_wf; decreasing_trivial_pre_omega
   loop 0
 
+@[inline]
+def findIdx (p : α → Bool) (as : Array α) : Nat := (as.findIdx? p).getD as.size
+
 @[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
-def indexOfAux [BEq α] (a : Array α) (v : α) (i : Nat) : Option (Fin a.size) :=
+def idxOfAux [BEq α] (a : Array α) (v : α) (i : Nat) : Option (Fin a.size) :=
   if h : i < a.size then
     if a[i] == v then some ⟨i, h⟩
-    else indexOfAux a v (i+1)
+    else idxOfAux a v (i+1)
   else none
 decreasing_by simp_wf; decreasing_trivial_pre_omega
 
-def indexOf? [BEq α] (a : Array α) (v : α) : Option (Fin a.size) :=
-  indexOfAux a v 0
+@[deprecated idxOfAux (since := "2025-01-29")]
+abbrev indexOfAux := @idxOfAux
+
+def finIdxOf? [BEq α] (a : Array α) (v : α) : Option (Fin a.size) :=
+  idxOfAux a v 0
 
-@[deprecated indexOf? (since := "2024-11-20")]
+@[deprecated "`Array.indexOf?` has been deprecated, use `idxOf?` or `finIdxOf?` instead." (since := "2025-01-29")]
+abbrev indexOf? := @finIdxOf?
+
+def idxOf? [BEq α] (a : Array α) (v : α) : Option Nat :=
+  (a.finIdxOf? v).map (·.val)
+
+@[deprecated idxOf? (since := "2024-11-20")]
 def getIdx? [BEq α] (a : Array α) (v : α) : Option Nat :=
   a.findIdx? fun a => a == v
 
@@ -857,15 +869,15 @@ def eraseIdx! (a : Array α) (i : Nat) : Array α :=
   if h : i < a.size then a.eraseIdx i h else panic! "invalid index"
 
 def erase [BEq α] (as : Array α) (a : α) : Array α :=
-  match as.indexOf? a with
+  match as.finIdxOf? a with
   | none   => as
   | some i => as.eraseIdx i
 
 /-- Erase the first element that satisfies the predicate `p`. -/
 def eraseP (as : Array α) (p : α → Bool) : Array α :=
-  match as.findIdx? p with
+  match as.findFinIdx? p with
   | none   => as
-  | some i => as.eraseIdxIfInBounds i
+  | some i => as.eraseIdx i
 
 /-- Insert element `a` at position `i`. -/
 @[inline] def insertIdx (as : Array α) (i : Nat) (a : α) (_ : i ≤ as.size := by get_elem_tactic) : Array α :=

src/Init/Data/Vector/Basic.lean

@@ -292,8 +292,16 @@ instance [BEq α] : BEq (Vector α n) where
 Finds the first index of a given value in a vector using `==` for comparison. Returns `none` if the
 no element of the index matches the given value.
 -/
-@[inline] def indexOf? [BEq α] (v : Vector α n) (x : α) : Option (Fin n) :=
-  (v.toArray.indexOf? x).map (Fin.cast v.size_toArray)
+@[inline] def finIdxOf? [BEq α] (v : Vector α n) (x : α) : Option (Fin n) :=
+  (v.toArray.finIdxOf? x).map (Fin.cast v.size_toArray)
+
+@[deprecated finIdxOf? (since := "2025-01-29")]
+abbrev indexOf? := @finIdxOf?
+
+/-- Finds the first index of a given value in a vector using a predicate. Returns `none` if the
+no element of the index matches the given value. -/
+@[inline] def findFinIdx? (v : Vector α n) (p : α → Bool) : Option (Fin n) :=
+  (v.toArray.findFinIdx? p).map (Fin.cast v.size_toArray)
 
 /-- Returns `true` when `v` is a prefix of the vector `w`. -/
 @[inline] def isPrefixOf [BEq α] (v : Vector α m) (w : Vector α n) : Bool :=

src/Init/Data/Vector/Lemmas.lean

@@ -101,8 +101,11 @@ theorem toArray_mk (a : Array α) (h : a.size = n) : (Vector.mk a h).toArray = a
 @[simp] theorem extract_mk (a : Array α) (h : a.size = n) (start stop) :
     (Vector.mk a h).extract start stop = Vector.mk (a.extract start stop) (by simp [h]) := rfl
 
-@[simp] theorem indexOf?_mk [BEq α] (a : Array α) (h : a.size = n) (x : α) :
-    (Vector.mk a h).indexOf? x = (a.indexOf? x).map (Fin.cast h) := rfl
+@[simp] theorem finIdxOf?_mk [BEq α] (a : Array α) (h : a.size = n) (x : α) :
+    (Vector.mk a h).finIdxOf? x = (a.finIdxOf? x).map (Fin.cast h) := rfl
+
+@[deprecated finIdxOf?_mk (since := "2025-01-29")]
+abbrev indexOf?_mk := @finIdxOf?_mk
 
 @[simp] theorem mk_isEqv_mk (r : α → α → Bool) (a b : Array α) (ha : a.size = n) (hb : b.size = n) :
     Vector.isEqv (Vector.mk a ha) (Vector.mk b hb) r = Array.isEqv a b r := by

src/Lean/Compiler/Specialize.lean

@@ -33,7 +33,7 @@ private def elabSpecArgs (declName : Name) (args : Array Syntax) : MetaM (Array
           result := result.push idx
       else
         let argName := arg.getId
-        if let some idx := argNames.indexOf? argName then
+        if let some idx := argNames.idxOf? argName then
           if result.contains idx then throwErrorAt arg "invalid specialization argument name `{argName}`, it has already been specified as a specialization candidate"
           result := result.push idx
         else

src/Lean/Data/PersistentHashMap.lean

@@ -231,7 +231,7 @@ def isUnaryNode : Node α β → Option (α × β)
 
 partial def eraseAux [BEq α] : Node α β → USize → α → Node α β
   | n@(Node.collision keys vals heq), _, k =>
-    match keys.indexOf? k with
+    match keys.finIdxOf? k with
     | some idx =>
       let keys' := keys.eraseIdx idx
       have keq := keys.size_eraseIdx idx _

src/Lean/Elab/App.lean

@@ -800,7 +800,7 @@ def getElabElimExprInfo (elimExpr : Expr) : MetaM ElabElimInfo := do
         throwError "unexpected number of arguments at motive type{indentExpr motiveType}"
       unless motiveResultType.isSort do
         throwError "motive result type must be a sort{indentExpr motiveType}"
-    let some motivePos ← pure (xs.indexOf? motive) |
+    let some motivePos ← pure (xs.idxOf? motive) |
       throwError "unexpected eliminator type{indentExpr elimType}"
     /-
     Compute transitive closure of fvars appearing in arguments to the motive.

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

@@ -292,7 +292,7 @@ def mkBrecOnApp (positions : Positions) (fnIdx : Nat) (brecOnConst : Nat → Exp
     let packedFTypes ← inferArgumentTypesN positions.size brecOn
     let packedFArgs ← positions.mapMwith PProdN.mkLambdas packedFTypes FArgs
     let brecOn := mkAppN brecOn packedFArgs
-    let some (size, idx) := positions.findSome? fun pos => (pos.size, ·) <$> pos.indexOf? fnIdx
+    let some (size, idx) := positions.findSome? fun pos => (pos.size, ·) <$> pos.finIdxOf? fnIdx
       | throwError "mkBrecOnApp: Could not find {fnIdx} in {positions}"
     let brecOn ← PProdN.projM size idx brecOn
     mkLambdaFVars ys (mkAppN brecOn otherArgs)

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

@@ -32,8 +32,8 @@ def prettyParameterSet (fnNames : Array Name) (xs : Array Expr) (values : Array
 private def getIndexMinPos (xs : Array Expr) (indices : Array Expr) : Nat := Id.run do
   let mut minPos := xs.size
   for index in indices do
-    match xs.indexOf? index with
-    | some pos => if pos.val < minPos then minPos := pos.val
+    match xs.idxOf? index with
+    | some pos => if pos < minPos then minPos := pos
     | _        => pure ()
   return minPos
 
@@ -91,8 +91,8 @@ def getRecArgInfo (fnName : Name) (numFixed : Nat) (xs : Array Expr) (i : Nat) :
             throwError "its type is an inductive datatype{indentExpr xType}\nand the datatype parameter{indentExpr indParam}\ndepends on the function parameter{indentExpr y}\nwhich does not come before the varying parameters and before the indices of the recursion parameter."
           | none =>
             let indAll := indInfo.all.toArray
-            let .some indIdx := indAll.indexOf? indInfo.name | panic! "{indInfo.name} not in {indInfo.all}"
-            let indicesPos := indIndices.map fun index => match xs.indexOf? index with | some i => i.val | none => unreachable!
+            let .some indIdx := indAll.idxOf? indInfo.name | panic! "{indInfo.name} not in {indInfo.all}"
+            let indicesPos := indIndices.map fun index => match xs.idxOf? index with | some i => i | none => unreachable!
             let indGroupInst := {
               IndGroupInfo.ofInductiveVal indInfo with
               levels := us
@@ -208,7 +208,7 @@ def argsInGroup (group : IndGroupInst) (xs : Array Expr) (value : Expr)
           if let some (_index, _y) ← hasBadIndexDep? ys indIndices then
             -- throwError "its type {indInfo.name} is an inductive family{indentExpr xType}\nand index{indentExpr index}\ndepends on the non index{indentExpr y}"
             continue
-          let indicesPos := indIndices.map fun index => match (xs++ys).indexOf? index with | some i => i.val | none => unreachable!
+          let indicesPos := indIndices.map fun index => match (xs++ys).idxOf? index with | some i => i | none => unreachable!
           return .some
             { fnName       := recArgInfo.fnName
               numFixed     := recArgInfo.numFixed

src/Lean/Elab/PreDefinition/TerminationMeasure.lean

@@ -90,7 +90,7 @@ def TerminationMeasure.elab (funName : Name) (type : Expr) (arity extraParams :
 def TerminationMeasure.structuralArg (measure : TerminationMeasure) : MetaM Nat := do
   assert! measure.structural
   lambdaTelescope measure.fn fun ys e => do
-    let .some idx := ys.indexOf? e
+    let .some idx := ys.idxOf? e
       | panic! "TerminationMeasure.structuralArg: body not one of the parameters"
     return idx
 

src/Lean/Elab/PreDefinition/WF/PackMutual.lean

@@ -48,7 +48,7 @@ def packCalls (fixedPrefix : Nat) (argsPacker : ArgsPacker) (funNames : Array Na
     let f := e.getAppFn
     if !f.isConst then
       return TransformStep.done e
-    if let some fidx := funNames.indexOf? f.constName! then
+    if let some fidx := funNames.idxOf? f.constName! then
       let arity := fixedPrefix + argsPacker.varNamess[fidx]!.size
       let e' ← withAppN arity e fun args => do
         let packedArg ← argsPacker.pack domain fidx args[fixedPrefix:]

src/Lean/Meta/Constructions/BRecOn.lean

@@ -195,14 +195,14 @@ private def buildBRecOnMinorPremise (rlvl : Level) (motives : Array Expr)
     let rec go (prods : Array Expr) : List Expr → MetaM Expr
       | [] => minor_type.withApp fun minor_type_fn minor_type_args => do
           let b ← PProdN.mk rlvl prods
-          let .some ⟨idx, _⟩ := motives.indexOf? minor_type_fn
+          let .some idx := motives.idxOf? minor_type_fn
             | throwError m!"Did not find {minor_type} in {motives}"
           mkPProdMk (mkAppN fs[idx]! (minor_type_args.push b)) b
       | arg::args => do
         let argType ← inferType arg
         forallTelescope argType fun arg_args arg_type => do
           arg_type.withApp fun arg_type_fn arg_type_args => do
-            if let .some idx := motives.indexOf? arg_type_fn then
+            if let .some idx := motives.idxOf? arg_type_fn then
               let name ← arg.fvarId!.getUserName
               let type' ← mkForallFVars arg_args
                 (← mkPProd arg_type (mkAppN belows[idx]! arg_type_args) )
@@ -264,7 +264,7 @@ private def mkBRecOnFromRec (recName : Name) (ind reflexive : Bool) (nParams : N
     let indices : Array Expr := refArgs[nParams + recVal.numMotives + recVal.numMinors:refArgs.size - 1]
     let major   : Expr       := refArgs[refArgs.size - 1]!
 
-    let some idx := motives.indexOf? refBody.getAppFn
+    let some idx := motives.idxOf? refBody.getAppFn
       | throwError "result type of {refType} is not one of {motives}"
 
     -- universe parameter of the type fomer.

src/Lean/Meta/FunInfo.lean

@@ -31,9 +31,9 @@ private def collectDeps (fvars : Array Expr) (e : Expr) : Array Nat :=
     | .proj _ _ e      => visit e deps
     | .mdata _ e       => visit e deps
     | .fvar ..         =>
-      match fvars.indexOf? e with
+      match fvars.idxOf? e with
       | none   => deps
-      | some i => if deps.contains i.val then deps else deps.push i.val
+      | some i => if deps.contains i then deps else deps.push i
     | _ => deps
   let deps := visit e #[]
   deps.qsort (fun i j => i < j)
@@ -82,7 +82,7 @@ private def getFunInfoAux (fn : Expr) (maxArgs? : Option Nat) : MetaM FunInfo :=
                   for h2 : i in [:args.size] do
                     if outParamPositions.contains i then
                       let arg := args[i]
-                      if let some idx := fvars.indexOf? arg then
+                      if let some idx := fvars.idxOf? arg then
                         if (← whnf (← inferType arg)).isForall then
                           paramInfo := paramInfo.modify idx fun info => { info with higherOrderOutParam := true }
                           higherOrderOutParams := higherOrderOutParams.insert arg.fvarId!

src/Lean/Meta/IndPredBelow.lean

@@ -562,7 +562,7 @@ where
 def findBelowIdx (xs : Array Expr) (motive : Expr) : MetaM $ Option (Expr × Nat) := do
   xs.findSomeM? fun x => do
   (← whnf (← inferType x)).withApp fun f _ =>
-  match f.constName?, xs.indexOf? x with
+  match f.constName?, xs.idxOf? x with
   | some name, some idx => do
     if (← isInductivePredicate name) then
       let (_, belowTy) ← belowType motive xs idx
@@ -571,7 +571,7 @@ def findBelowIdx (xs : Array Expr) (motive : Expr) : MetaM $ Option (Expr × Nat
         trace[Meta.IndPredBelow.match] "{←Meta.ppGoal below.mvarId!}"
         if (← below.mvarId!.applyRules { backtracking := false, maxDepth := 1 } []).isEmpty then
           trace[Meta.IndPredBelow.match] "Found below term in the local context: {below}"
-          if (← xs.anyM (isDefEq below)) then pure none else pure (below, idx.val)
+          if (← xs.anyM (isDefEq below)) then pure none else pure (below, idx)
         else
           trace[Meta.IndPredBelow.match] "could not find below term in the local context"
           pure none

src/Lean/Meta/Match/Match.lean

@@ -751,9 +751,9 @@ private partial def process (p : Problem) : StateRefT State MetaM Unit := do
 private def getUElimPos? (matcherLevels : List Level) (uElim : Level) : MetaM (Option Nat) :=
   if uElim == levelZero then
     return none
-  else match matcherLevels.toArray.indexOf? uElim with
+  else match matcherLevels.idxOf? uElim with
     | none => throwError "dependent match elimination failed, universe level not found"
-    | some pos => return some pos.val
+    | some pos => return some pos
 
 /- See comment at `mkMatcher` before `mkAuxDefinition` -/
 register_builtin_option bootstrap.genMatcherCode : Bool := {

src/Lean/Meta/Match/MatchEqs.lean

@@ -129,9 +129,9 @@ where
           let typeNew := b.instantiate1 y
           if let some (_, lhs, rhs) ← matchEq? d then
             if lhs.isFVar && ys.contains lhs && args.contains lhs && isNamedPatternProof typeNew y then
-               let some j  := ys.indexOf? lhs | unreachable!
+               let some j  := ys.finIdxOf? lhs | unreachable!
                let ys      := ys.eraseIdx j
-               let some k  := args.indexOf? lhs | unreachable!
+               let some k  := args.idxOf? lhs | unreachable!
                let mask    := mask.set! k false
                let args    := args.map fun arg => if arg == lhs then rhs else arg
                let arg     ← mkEqRefl rhs

src/Lean/Meta/RecursorInfo.lean

@@ -107,7 +107,7 @@ private def getMajorPosDepElim (declName : Name) (majorPos? : Option Nat) (xs :
     if motiveArgs.isEmpty then
       throwError "invalid user defined recursor, '{declName}' does not support dependent elimination, and position of the major premise was not specified (solution: set attribute '[recursor <pos>]', where <pos> is the position of the major premise)"
     let major := motiveArgs.back!
-    match xs.indexOf? major with
+    match xs.idxOf? major with
     | some majorPos => pure (major, majorPos, true)
     | none          => throwError "ill-formed recursor '{declName}'"
 

src/Lean/Meta/Tactic/ElimInfo.lean

@@ -60,12 +60,12 @@ def getElimExprInfo (elimExpr : Expr) (baseDeclName? : Option Name := none) : Me
         throwError "unexpected number of arguments at motive type{indentExpr motiveType}"
       unless motiveResultType.isSort do
         throwError "motive result type must be a sort{indentExpr motiveType}"
-    let some motivePos ← pure (xs.indexOf? motive) |
+    let some motivePos ← pure (xs.idxOf? motive) |
       throwError "unexpected eliminator type{indentExpr elimType}"
     let targetsPos ← targets.mapM fun target => do
-      match xs.indexOf? target with
+      match xs.idxOf? target with
       | none => throwError "unexpected eliminator type{indentExpr elimType}"
-      | some targetPos => pure targetPos.val
+      | some targetPos => pure targetPos
     let mut altsInfo := #[]
     let env ← getEnv
     for h : i in [:xs.size] do

src/Lean/Meta/Tactic/FunInd.lean

@@ -982,7 +982,7 @@ def deriveInductionStructural (names : Array Name) (numFixed : Nat) : MetaM Unit
           let fns := infos.map fun info =>
             mkAppN (.const info.name (info.levelParams.map mkLevelParam)) xs
           let isRecCall : Expr → Option Expr := fun e => do
-            if let .some i := motives.indexOf? e.getAppFn then
+            if let .some i := motives.idxOf? e.getAppFn then
               if e.getAppNumArgs = motiveArities[i]! then
                 return mkAppN fns[i]! e.getAppArgs
             .none