chore: naming convention

src/Init/Data/Array/Basic.lean

@@ -647,7 +647,7 @@ partial def indexOfAux {α} [HasBeq α] (a : Array α) (v : α) : Nat → Option
     else indexOfAux (i+1)
   else none
 
-def indexOf {α} [HasBeq α] (a : Array α) (v : α) : Option (Fin a.size) :=
+def indexOf? {α} [HasBeq α] (a : Array α) (v : α) : Option (Fin a.size) :=
 indexOfAux a v 0
 
 partial def eraseIdxAux {α} : Nat → Array α → Array α
@@ -697,7 +697,7 @@ def elem [HasBeq α] (a : α) (as : Array α) : Bool :=
 as.contains a
 
 def erase [HasBeq α] (as : Array α) (a : α) : Array α :=
-match as.indexOf a with
+match as.indexOf? a with
 | none   => as
 | some i => as.feraseIdx i
 

src/Lean/Elab/PreDefinition/Structural.lean

@@ -39,7 +39,7 @@ structure RecArgInfo :=
 
 private def getIndexMinPos (xs : Array Expr) (indices : Array Expr) : Nat :=
 indices.foldl
-  (fun minPos index => match xs.indexOf index with
+  (fun minPos index => match xs.indexOf? index with
     | some pos => if pos.val < minPos then pos.val else minPos
     | _        => minPos)
   xs.size
@@ -115,7 +115,7 @@ private partial def findRecArgAux {α} (numFixed : Nat) (xs : Array Expr) (k : R
                   Format.line ++ "depends on" ++ indentExpr y)
                 (findRecArgAux (i+1))
             | none => do
-              let indicesPos := indIndices.map fun index => match ys.indexOf index with | some i => i.val | none => unreachable!;
+              let indicesPos := indIndices.map fun index => match ys.indexOf? index with | some i => i.val | none => unreachable!;
               orelseMergeErrors
                 (k { fixedParams := fixedParams, ys := ys, pos := i - fixedParams.size,
                      indicesPos  := indicesPos,

src/Lean/Meta/FunInfo.lean

@@ -30,7 +30,7 @@ private def collectDepsAux (fvars : Array Expr) : Expr → Array Nat → Array N
 | Expr.proj _ _ e _,        deps => collectDepsAux e deps
 | Expr.mdata _ e _,         deps => collectDepsAux e deps
 | e@(Expr.fvar _ _),        deps =>
-  match fvars.indexOf e with
+  match fvars.indexOf? e with
   | none   => deps
   | some i => if deps.contains i.val then deps else deps.push i.val
 | _,                        deps => deps

src/Std/Data/PersistentHashMap.lean

@@ -225,7 +225,7 @@ def isUnaryNode : Node α β → Option (α × β)
 
 partial def eraseAux [HasBeq α] : Node α β → USize → α → Node α β × Bool
 | n@(Node.collision keys vals heq), _, k =>
-  match keys.indexOf k with
+  match keys.indexOf? k with
   | some idx =>
     let ⟨keys', keq⟩ := keys.eraseIdx' idx;
     let ⟨vals', veq⟩ := vals.eraseIdx' (Eq.rec idx heq);

tests/compiler/phashmap2.lean

@@ -28,7 +28,7 @@ partial def formatMap : Node Nat Nat → Format
 def main : IO Unit :=
 do
 let a : Array Nat := [1, 2, 3].toArray;
-IO.println (a.indexOf 2);
+IO.println (a.indexOf? 2);
 let m : Map := PersistentHashMap.empty;
 let m := m.insert 1 1;
 let m := m.insert 33 2;