Try to remove some nolints

leanprover-community · Aug 21, 2024 · 4b976ec · 4b976ec
1 parent 0cbb129
commit 4b976ec
Show file tree

Hide file tree

Showing 2 changed files with 0 additions and 3 deletions.
diff --git a/Mathlib/Computability/Primrec.lean b/Mathlib/Computability/Primrec.lean
@@ -58,8 +58,6 @@ namespace Nat
 @[simp, reducible]
 def unpaired {α} (f : ℕ → ℕ → α) (n : ℕ) : α :=
   f n.unpair.1 n.unpair.2
-attribute [nolint simpVarHead] unpaired.eq_1
-
 
 /-- The primitive recursive functions `ℕ → ℕ`. -/
 protected inductive Primrec : (ℕ → ℕ) → Prop

diff --git a/Mathlib/Logic/Function/Basic.lean b/Mathlib/Logic/Function/Basic.lean
@@ -25,7 +25,6 @@ variable {α β γ : Sort*} {f : α → β}
 /-- Evaluate a function at an argument. Useful if you want to talk about the partially applied
   `Function.eval x : (∀ x, β x) → β x`. -/
 @[reducible, simp] def eval {β : α → Sort*} (x : α) (f : ∀ x, β x) : β x := f x
-attribute [nolint simpVarHead] eval.eq_1
 
 theorem eval_apply {β : α → Sort*} (x : α) (f : ∀ x, β x) : eval x f = f x :=
   rfl