Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - chore: classify new instance porting notes #11433

Closed
wants to merge 3 commits into from
Closed

[Merged by Bors] - chore: classify new instance porting notes #11433

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
32631c2
chore: classify `added instance` porting notes
pitmonticone Mar 1, 2024
7d64cb2
chore: classify `added instance` porting notes
pitmonticone Mar 16, 2024
d876920
Merge branch 'master' into pitmonticone/added-instance
pitmonticone Mar 16, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion Mathlib/Data/Nat/PartENat.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
2 changes: 1 addition & 1 deletion Mathlib/Data/PNat/Defs.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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⟩⟩

Expand Down
2 changes: 1 addition & 1 deletion Mathlib/InformationTheory/Hamming.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 _
Expand Down
2 changes: 1 addition & 1 deletion Mathlib/Init/Order/Defs.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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⟩
Expand Down
Loading