Zulip Chat Archive

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: Aug 03 2023 at 10:10 UTC