From f2f41de14b32360a9b4e731dfb935f38d897ec85 Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Mon, 25 Mar 2024 02:18:45 +0000 Subject: [PATCH] chore: rm @[eqns] in SetTheory/Ordinal/Notation (#11646) Co-authored-by: Scott Morrison --- Mathlib/SetTheory/Ordinal/Notation.lean | 12 +++++------- 1 file changed, 5 insertions(+), 7 deletions(-) diff --git a/Mathlib/SetTheory/Ordinal/Notation.lean b/Mathlib/SetTheory/Ordinal/Notation.lean index 2049b700e6bb5..ee2d22f9db5d6 100644 --- a/Mathlib/SetTheory/Ordinal/Notation.lean +++ b/Mathlib/SetTheory/Ordinal/Notation.lean @@ -127,18 +127,16 @@ def ofNat : ℕ → ONote | Nat.succ n => oadd 0 n.succPNat 0 #align onote.of_nat ONote.ofNat --- Porting note: the generated simp lemmas of `ofNat` is not good so we replace. +-- Adaptation note: +-- During the port we marked these lemmas with `@[eqns]` to emulate the old Lean 3 behaviour. +-- See https://github.com/leanprover-community/mathlib4/issues/11647 -theorem ofNat_zero : ofNat 0 = 0 := +@[simp] theorem ofNat_zero : ofNat 0 = 0 := rfl -theorem ofNat_succ (n) : ofNat (Nat.succ n) = oadd 0 n.succPNat 0 := +@[simp] theorem ofNat_succ (n) : ofNat (Nat.succ n) = oadd 0 n.succPNat 0 := rfl -attribute [eqns ofNat_zero ofNat_succ] ofNat - -attribute [simp] ofNat - instance nat (n : ℕ) : OfNat ONote n where ofNat := ofNat n