Skip to content

Commit e2aa6cc

Browse files
kim-emalgebraic-dev
authored andcommitted
chore: add missing List.eraseIdx_insertIdx deprecation (leanprover#8863)
1 parent efd379e commit e2aa6cc

File tree

1 file changed

+3
-0
lines changed

1 file changed

+3
-0
lines changed

src/Init/Data/List/Nat/InsertIdx.lean

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -120,6 +120,9 @@ theorem eraseIdx_insertIdx_self {i : Nat} {l : List α} (a : α) : (l.insertIdx
120120
rw [eraseIdx_eq_modifyTailIdx, insertIdx, modifyTailIdx_modifyTailIdx_self]
121121
exact modifyTailIdx_id _ _
122122

123+
@[deprecated eraseIdx_insertIdx_self (since := "2025-06-18")]
124+
abbrev eraseIdx_insertIdx := @eraseIdx_insertIdx_self
125+
123126
@[simp]
124127
theorem insertIdx_length_self {l : List α} {x : α} : l.insertIdx l.length x = l ++ [x] := by
125128
induction l with

0 commit comments

Comments
 (0)