Root Exports

Stream: Is there code for X?

[Mac]

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

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

BTW, #xy #mwe

[Yury G. Kudryashov]

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)?

[Bryan Gin-ge Chen]

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.)

[Yury G. Kudryashov]

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.

[Eric Wieser]

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

[Mac]

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?

[Eric Wieser]

Are you taking about lean 3 or lean 4?

[Eric Wieser]

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

[Mario Carneiro]

Actually has_add was renamed to Add

[Mario Carneiro]

the has_* classes lost the Has

[Mac]

Yeah, my use case is in lean 4.

[Eric Wieser]

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