Zulip Chat Archive

Stream: new members

Topic: Hiding imports

Pedro Minicz (Oct 21 2020 at 02:14):

What is the equivalent of Haskell's import X hiding (x1, x2, x2)?

Pedro Minicz (Oct 21 2020 at 02:15):

Particularly, I would like to import tactic and define my own class named ring.

Reid Barton (Oct 21 2020 at 02:17):

There isn't one. See recent discussion at https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/import.20specific.20lemma.20from.20mathlib/near/213172285

Last updated: Dec 20 2023 at 11:08 UTC