Skip to content

Commit

Permalink
fix: name collision on Countable.toSmall (#11914)
Browse files Browse the repository at this point in the history
This is currently causing mathport to fail, it's a new kind of name collision that has not occurred before: two definitions made in two different files are being `#align`ed to the same thing. Normally mathport will automatically rename one of them but in this case neither one imports the other so it doesn't know to avoid the situation.



Co-authored-by: Mario Carneiro <di.gama@gmail.com>
  • Loading branch information
digama0 and digama0 committed Apr 5, 2024
1 parent 8b50609 commit 1d98eca
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion Mathlib/Data/Countable/Small.lean
Expand Up @@ -22,7 +22,7 @@ instance (priority := 100) Countable.toSmall (α : Type v) [Countable α] : Smal
let ⟨_, hf⟩ := exists_injective_nat α
small_of_injective hf
#align small_of_countable Countable.toSmall
#align small_of_fintype Countable.toSmall
#align small_of_fintype Countable.toSmallₓ -- this alignment clashes with the one above

@[deprecated, nolint defLemma] -- 2024-03-20
alias small_of_countable := Countable.toSmall
Expand Down

0 comments on commit 1d98eca

Please sign in to comment.