temporary nolints

leanprover-community · Sep 6, 2024 · 8e11f3b · 8e11f3b
1 parent 78cc6f0
commit 8e11f3b
Show file tree

Hide file tree

Showing 2 changed files with 10 additions and 2 deletions.
diff --git a/Mathlib/Data/List/Basic.lean b/Mathlib/Data/List/Basic.lean
@@ -945,7 +945,11 @@ theorem infix_bind_of_mem {a : α} {as : List α} (h : a ∈ as) (f : α → Lis
 theorem map_eq_map {α β} (f : α → β) (l : List α) : f <$> l = map f l :=
   rfl
 
-@[simp]
+#adaptation_note
+/--
+`nolint simpNF` should be removed after nightly-2024-09-07.
+-/
+@[simp, nolint simpNF]
 theorem map_tail (f : α → β) (l) : map f (tail l) = tail (map f l) := by cases l <;> rfl
 
 /-- A single `List.map` of a composition of functions is equal to

diff --git a/Mathlib/Data/List/Infix.lean b/Mathlib/Data/List/Infix.lean
@@ -160,7 +160,11 @@ This can be removed after nightly-2024-09-07.
 -/
 attribute [-simp] map_tail
 
-@[simp]
+#adaptation_note
+/--
+`nolint simpNF` should be removed after nightly-2024-09-07.
+-/
+@[simp, nolint simpNF]
 theorem inits_append : ∀ s t : List α, inits (s ++ t) = s.inits ++ t.inits.tail.map fun l => s ++ l
   | [], [] => by simp
   | [], a :: t => by simp