import renaming?

Stream: general

[Scott Morrison]

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

[Mario Carneiro]

I don't think there is such a thing

[Mario Carneiro]

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

[Patrick Massot]

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

[Scott Morrison]

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]

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

[Johan Commelin]

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

[Sebastian Ullrich]

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.