Skip to content

Commit 810f0ec

Browse files
committed
chore: deprecate Array.modifyOp
1 parent 538b7f2 commit 810f0ec

File tree

1 file changed

+1
-3
lines changed

1 file changed

+1
-3
lines changed

src/Init/Data/Array/Basic.lean

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -275,9 +275,7 @@ def modifyM [Monad m] (a : Array α) (i : Nat) (f : α → m α) : m (Array α)
275275
def modify (a : Array α) (i : Nat) (f : α → α) : Array α :=
276276
Id.run <| modifyM a i f
277277

278-
@[inline]
279-
def modifyOp (self : Array α) (idx : Nat) (f : α → α) : Array α :=
280-
self.modify idx f
278+
@[deprecated modify (since := "2024-10-22")] abbrev modifyOp := @modify
281279

282280
/--
283281
We claim this unsafe implementation is correct because an array cannot have more than `usizeSz` elements in our runtime.

0 commit comments

Comments
 (0)