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
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
Simon Hudon (Feb 07 2019 at 04:22):
Oh you're right, sorry! I misread!
Last updated: May 10 2021 at 00:31 UTC