chore: deprecate Array.modifyOp

src/Init/Data/Array/Basic.lean

@@ -275,9 +275,7 @@ def modifyM [Monad m] (a : Array α) (i : Nat) (f : α → m α) : m (Array α)
 def modify (a : Array α) (i : Nat) (f : α → α) : Array α :=
   Id.run <| modifyM a i f
 
-@[inline]
-def modifyOp (self : Array α) (idx : Nat) (f : α → α) : Array α :=
-  self.modify idx f
+@[deprecated modify (since := "2024-10-22")] abbrev modifyOp := @modify
 
 /--
   We claim this unsafe implementation is correct because an array cannot have more than `usizeSz` elements in our runtime.

src/Lean/Elab/StructInst.lean

@@ -184,7 +184,7 @@ private def elabModifyOp (stx modifyOp : Syntax) (sources : Array ExplicitSource
     let lval := modifyOp[0][0]
     let idx  := lval[1]
     let self := sources[0]!.stx
-    let stxNew ← `($(self).modifyOp (idx := $idx) (fun s => $val))
+    let stxNew ← `($(self).modify (i := $idx) (fun s => $val))
     trace[Elab.struct.modifyOp] "{stx}\n===>\n{stxNew}"
     withMacroExpansion stx stxNew <| elabTerm stxNew expectedType?
   let rest := modifyOp[0][1]