## Stream: general

### Topic: import renaming?

#### Scott Morrison (Aug 09 2018 at 09:43):

can someone point me to the syntax for import renaming? I can't find it. :-(

#### Mario Carneiro (Aug 09 2018 at 09:43):

I don't think there is such a thing

#### Mario Carneiro (Aug 09 2018 at 09:44):

I think it was proposed for lean 4, but AFAIK it can't be done in lean 3

#### Patrick Massot (Aug 09 2018 at 09:44):

People often talk about it here, but only to wish it exists

#### Scott Morrison (Aug 09 2018 at 09:44):

oh, wow, maybe I dreamt it. I have a really strong memory of yesterday learning that you could hide and rename individual declarations when you made an import!

#### Mario Carneiro (Aug 09 2018 at 09:45):

There is open and hide, which have a syntax for opening individual declarations and renaming

#### Johan Commelin (Aug 09 2018 at 09:47):

I don't think you learnt that here...

#### Sebastian Ullrich (Aug 09 2018 at 17:02):

Declarations in a Lean environment aren't grouped by modules, so I don't see how this would be implemented without fundamentally changing the architecture. Which we don't plan to do, afaik.

Last updated: May 13 2021 at 05:21 UTC