Zulip Chat Archive

Stream: new members

Topic: Hiding imports


view this post on Zulip Pedro Minicz (Oct 21 2020 at 02:14):

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

view this post on Zulip Pedro Minicz (Oct 21 2020 at 02:15):

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

view this post on Zulip 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: May 15 2021 at 22:14 UTC