export renaming

Stream: general

[Yury G. Kudryashov]

Is it possible to export one name from a namespace while renaming it?

[Chris B]

Not sure, but if it helps, you can do the renaming when you import it instead.

open foo (renaming bar -> baz)

[Eric Wieser]

Is there any way to use export foo (renaming ...) without having to add (hiding every name under the sun)? In #8918 I wrote

export mul_distrib_mul_action (smul_one) mul_distrib_mul_action (renaming smul_mul → smul_mul')

which I hoped would mean "export smul_one as smul_one and smul_mul as smul_mul'", but it actually mean "export everything except rename smul_mul to smul_mul'.

Is there a spelling I've missed?

[Mario Carneiro]

the syntax exists, it is export mul_distrib_mul_action (smul_one) (renaming smul_mul → smul_mul'), but it is rejected with

invalid 'open/export' command option, mixing explicit and implicit 'open/export' options

[Mario Carneiro]

Note that fancy export options are on the lean 4 chopping block, so you are probably best off doing something else