lean4
lean4 copied to clipboard
fix: hygienic resolution of namespaces
As noticed in https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Changing.20instance.20priority/near/292252231
@Kha Could you please rebase this PR when you have time?