Zulip Chat Archive

Stream: new members

Topic: global namespace qualifier?

Duckki Oe (Nov 23 2020 at 22:58):

When there is a naming conflict of "abs" and "complex.abs", how can I tell lean to use the global "abs", instead of "complex.abs"?

Reid Barton (Nov 23 2020 at 22:59):

_root_.abs

Duckki Oe (Nov 23 2020 at 23:02):

thanks!

Last updated: Dec 20 2023 at 11:08 UTC