chore: classify new instance porting notes (#11433)

Classifies by adding issue number #10754 to porting notes claiming "new instance".
leanprover-community · Apr 16, 2024 · f22bad9 · f22bad9
1 parent 8655f13
commit f22bad9
Show file tree

Hide file tree

Showing 4 changed files with 4 additions and 4 deletions.
diff --git a/Mathlib/Data/Nat/PartENat.lean b/Mathlib/Data/Nat/PartENat.lean
@@ -680,7 +680,7 @@ def ofENat : ℕ∞ → PartENat :=
   | Option.none => none
   | Option.some n => some n
 
--- Porting note: new
+-- Porting note (#10754): new instance
 instance : Coe ℕ∞ PartENat := ⟨ofENat⟩
 
 -- Porting note: new. This could probably be moved to tests or removed.

diff --git a/Mathlib/Data/PNat/Defs.lean b/Mathlib/Data/PNat/Defs.lean
@@ -44,7 +44,7 @@ instance coePNatNat : Coe ℕ+ ℕ :=
 instance : Repr ℕ+ :=
   ⟨fun n n' => reprPrec n.1 n'⟩
 
--- Porting note: New instance not in Lean3
+--Porting note (#10754): New instance not in Lean3
 instance (n : ℕ) : OfNat ℕ+ (n+1) :=
   ⟨⟨n + 1, Nat.succ_pos n⟩⟩
 

diff --git a/Mathlib/InformationTheory/Hamming.lean b/Mathlib/InformationTheory/Hamming.lean
@@ -450,7 +450,7 @@ theorem nndist_eq_hammingDist (x y : Hamming β) :
   rfl
 #align hamming.nndist_eq_hamming_dist Hamming.nndist_eq_hammingDist
 
--- Porting note: new
+-- Porting note (#10754): new instance
 instance : DiscreteTopology (Hamming β) := ⟨rfl⟩
 
 instance : MetricSpace (Hamming β) := .ofT0PseudoMetricSpace _

diff --git a/Mathlib/Init/Order/Defs.lean b/Mathlib/Init/Order/Defs.lean
@@ -129,7 +129,7 @@ theorem gt_of_ge_of_gt {a b c : α} (h₁ : a ≥ b) (h₂ : b > c) : a > c :=
   lt_of_lt_of_le h₂ h₁
 #align gt_of_ge_of_gt gt_of_ge_of_gt
 
--- Porting note: new
+-- Porting note (#10754): new instance
 instance (priority := 900) : @Trans α α α LE.le LE.le LE.le := ⟨le_trans⟩
 instance (priority := 900) : @Trans α α α LT.lt LT.lt LT.lt := ⟨lt_trans⟩
 instance (priority := 900) : @Trans α α α LT.lt LE.le LT.lt := ⟨lt_of_lt_of_le⟩