leanprover · kim-em · Oct 21, 2024 · Oct 21, 2024 · Oct 21, 2024
@@ -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.

diff --git a/src/Lean/Elab/StructInst.lean b/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]

diff --git a/stage0/src/kernel/declaration.cpp b/stage0/src/kernel/declaration.cpp
diff --git a/stage0/src/kernel/declaration.h b/stage0/src/kernel/declaration.h
diff --git a/stage0/src/kernel/expr.cpp b/stage0/src/kernel/expr.cpp
diff --git a/stage0/src/kernel/expr.h b/stage0/src/kernel/expr.h
diff --git a/stage0/src/kernel/inductive.h b/stage0/src/kernel/inductive.h
diff --git a/stage0/stdlib/Init.c b/stage0/stdlib/Init.c
diff --git a/stage0/stdlib/Init/Data/Array.c b/stage0/stdlib/Init/Data/Array.c