hiding from prelude

Stream: new members

[Hans-Dieter Hiep]

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

[Rob Lewis]

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]

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

[Simon Hudon]

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]

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]

Oh you're right, sorry! I misread!