Stream: new members

Topic: hiding from prelude

Hans-Dieter Hiep (Feb 06 2019 at 17:28):

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

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.

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.

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.

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.

Simon Hudon (Feb 07 2019 at 04:22):

Oh you're right, sorry! I misread!

Last updated: May 10 2021 at 00:31 UTC