Zulip Chat Archive

Stream: new members

Topic: hiding from prelude


view this post on Zulip Hans-Dieter Hiep (Feb 06 2019 at 17:28):

How do you hide symbols from the prelude? In particular, how does one hide field?

view this post on Zulip Rob Lewis (Feb 06 2019 at 18:01):

You don't, for the most part. One option is to work in a new namespace, so you can reuse the name field, but this might occasionally lead to confusion. Using the prelude command at the top of your file will prevent Lean from loading anything from core, and then you can manually import things from init. But I doubt you can import very much without getting field, certainly nothing from mathlib.

view this post on Zulip Hans-Dieter Hiep (Feb 06 2019 at 18:18):

Thanks! Makes a lot of sense to work within a namespace then, since I do import other things from mathlib.

view this post on Zulip Simon Hudon (Feb 06 2019 at 20:41):

I think there's an asterisk on your answer @Rob Lewis. If your file starts with prelude, Lean doesn't implicitly import init. But as you say, if you're trying avoid name clashes, that's not the way to go.

view this post on Zulip Rob Lewis (Feb 06 2019 at 20:47):

Hmm? That's what I said, or it's what I meant, anyway. You can start with prelude and then import things manually, but you can't import anything that imports init.algebra.field.

view this post on Zulip Simon Hudon (Feb 07 2019 at 04:22):

Oh you're right, sorry! I misread!


Last updated: May 10 2021 at 00:31 UTC