lean4 icon indicating copy to clipboard operation
lean4 copied to clipboard

fix: hygienic resolution of namespaces

Open Kha opened this issue 3 years ago • 1 comments

As noticed in https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Changing.20instance.20priority/near/292252231

Kha avatar Aug 07 '22 14:08 Kha

@Kha Could you please rebase this PR when you have time?

leodemoura avatar Aug 14 '22 01:08 leodemoura