nolint attributes

leanprover-community · Aug 19, 2024 · e6ce4b5 · e6ce4b5
1 parent e24f1c6
commit e6ce4b5
Show file tree

Hide file tree

Showing 7 changed files with 13 additions and 2 deletions.
diff --git a/Mathlib/CategoryTheory/WithTerminal.lean b/Mathlib/CategoryTheory/WithTerminal.lean
@@ -70,6 +70,7 @@ def Hom : WithTerminal C → WithTerminal C → Type v
   | of X, of Y => X ⟶ Y
   | star, of _ => PEmpty
   | _, star => PUnit
+attribute [nolint simpNF] Hom.eq_3
 
 /-- Identity morphisms for `WithTerminal C`. -/
 @[simp]
@@ -85,6 +86,8 @@ def comp : ∀ {X Y Z : WithTerminal C}, Hom X Y → Hom Y Z → Hom X Z
   | star, of _X, _ => fun f _g => PEmpty.elim f
   | _, star, of _Y => fun _f g => PEmpty.elim g
   | star, star, star => fun _ _ => PUnit.unit
+attribute [nolint simpNF] comp.eq_3
+attribute [nolint simpNF] comp.eq_4
 
 instance : Category.{v} (WithTerminal C) where
   Hom X Y := Hom X Y
@@ -371,6 +374,7 @@ def Hom : WithInitial C → WithInitial C → Type v
   | of X, of Y => X ⟶ Y
   | of _, _ => PEmpty
   | star, _ => PUnit
+attribute [nolint simpNF] Hom.eq_2
 
 /-- Identity morphisms for `WithInitial C`. -/
 @[simp]
@@ -386,6 +390,8 @@ def comp : ∀ {X Y Z : WithInitial C}, Hom X Y → Hom Y Z → Hom X Z
   | _, of _X, star => fun _f g => PEmpty.elim g
   | of _Y, star, _ => fun f _g => PEmpty.elim f
   | star, star, star => fun _ _ => PUnit.unit
+attribute [nolint simpNF] comp.eq_3
+attribute [nolint simpNF] comp.eq_4
 
 instance : Category.{v} (WithInitial C) where
   Hom X Y := Hom X Y

diff --git a/Mathlib/Computability/Primrec.lean b/Mathlib/Computability/Primrec.lean
@@ -55,10 +55,11 @@ namespace Nat
 --   n.cases a f = n.casesOn a f := rfl
 
 /-- Calls the given function on a pair of entries `n`, encoded via the pairing function. -/
-@[simp, reducible]
+@[simp, reducible, nolint simpVarHead]
 def unpaired {α} (f : ℕ → ℕ → α) (n : ℕ) : α :=
   f n.unpair.1 n.unpair.2
 
+
 /-- The primitive recursive functions `ℕ → ℕ`. -/
 protected inductive Primrec : (ℕ → ℕ) → Prop
   | zero : Nat.Primrec fun _ => 0

diff --git a/Mathlib/Computability/TMToPartrec.lean b/Mathlib/Computability/TMToPartrec.lean
@@ -898,6 +898,7 @@ def natEnd : Γ' → Bool
   | Γ'.consₗ => true
   | Γ'.cons => true
   | _ => false
+attribute [nolint simpNF] natEnd.eq_3
 
 /-- Pop a value from the stack and place the result in local store. -/
 @[simp]

diff --git a/Mathlib/Data/Seq/Computation.lean b/Mathlib/Data/Seq/Computation.lean
@@ -246,6 +246,7 @@ def BisimO : α ⊕ (Computation α) → α ⊕ (Computation α) → Prop
   | _, _ => False
 
 attribute [simp] BisimO
+attribute [nolint simpNF] BisimO.eq_3
 
 /-- Attribute expressing bisimilarity over two `Computation`s-/
 def IsBisimulation :=

diff --git a/Mathlib/Data/Seq/Seq.lean b/Mathlib/Data/Seq/Seq.lean
@@ -315,6 +315,7 @@ def BisimO : Option (Seq1 α) → Option (Seq1 α) → Prop
   | _, _ => False
 
 attribute [simp] BisimO
+attribute [nolint simpNF] BisimO.eq_3
 
 /-- a relation is bisimilar if it meets the `BisimO` test-/
 def IsBisimulation :=

diff --git a/Mathlib/Data/Seq/WSeq.lean b/Mathlib/Data/Seq/WSeq.lean
@@ -394,6 +394,7 @@ def LiftRelO (R : α → β → Prop) (C : WSeq α → WSeq β → Prop) :
   | none, none => True
   | some (a, s), some (b, t) => R a b ∧ C s t
   | _, _ => False
+attribute [nolint simpNF] LiftRelO.eq_3
 
 theorem LiftRelO.imp {R S : α → β → Prop} {C D : WSeq α → WSeq β → Prop} (H1 : ∀ a b, R a b → S a b)
     (H2 : ∀ s t, C s t → D s t) : ∀ {o p}, LiftRelO R C o p → LiftRelO S D o p

diff --git a/Mathlib/Logic/Function/Basic.lean b/Mathlib/Logic/Function/Basic.lean
@@ -24,7 +24,7 @@ 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
+@[reducible, simp, nolint simpVarHead] def eval {β : α → Sort*} (x : α) (f : ∀ x, β x) : β x := f x
 
 theorem eval_apply {β : α → Sort*} (x : α) (f : ∀ x, β x) : eval x f = f x :=
   rfl