Zulip Chat Archive

Stream: Is there code for X?

Topic: Root Exports


view this post on Zulip Mac (Mar 29 2021 at 02:53):

Is there any way to export names from the root namespace into other namespaces?

view this post on Zulip Yury G. Kudryashov (Mar 29 2021 at 03:06):

export doesn't create a new name. It just makes the old name available without an explicit prefix.

view this post on Zulip Yury G. Kudryashov (Mar 29 2021 at 03:06):

If you want to have a new def, then you can create an alias (either manually or using alias command).

view this post on Zulip Yury G. Kudryashov (Mar 29 2021 at 03:07):

BTW, #xy #mwe

view this post on Zulip Yury G. Kudryashov (Mar 29 2021 at 03:08):

What exactly do you want to achieve (i.e., what code doesn't work now and should work after some non-existing export_from_root my_name my_ns command)?

view this post on Zulip Bryan Gin-ge Chen (Mar 29 2021 at 03:10):

In mathlib we have some really convenient root declarations that have aliases in a namespace at the beginning of algebra.order. (These are all created using tactic#alias.)

view this post on Zulip Yury G. Kudryashov (Mar 29 2021 at 03:13):

That's why I asked for an #mwe: if we're talking about a lemma, then sometimes it makes sense to create an alias (e.g., to allow dot notation). If we're talking about a def, then creating an alias creates a new definition, and Lean won't know that they are the same thing.

view this post on Zulip Eric Wieser (Mar 29 2021 at 09:32):

Why don't we just use export everywhere instead of alias? Does it not work for dot notation?

view this post on Zulip Mac (Apr 05 2021 at 02:20):

My problem is the following: I have a namespace Gaea.Math and I would like to export the root Add into the namespace so that I can access it by Gaea.Math.Add (or from within the Gaea namespace itself by Math.Add). Does that make sense?

view this post on Zulip Eric Wieser (Apr 05 2021 at 09:17):

Are you taking about lean 3 or lean 4?

view this post on Zulip Eric Wieser (Apr 05 2021 at 09:18):

(since 3's has_add is 4's HasAdd, and you're taking about Add)

view this post on Zulip Mario Carneiro (Apr 05 2021 at 10:14):

Actually has_add was renamed to Add

view this post on Zulip Mario Carneiro (Apr 05 2021 at 10:14):

the has_* classes lost the Has

view this post on Zulip Mac (Apr 06 2021 at 20:45):

Yeah, my use case is in lean 4.

view this post on Zulip Eric Wieser (Apr 06 2021 at 20:59):

Then you might do better to ask in #lean4, but I'd recommend preparing a full #mwe before posting there.


Last updated: May 07 2021 at 22:14 UTC