Zulip Chat Archive

Stream: general

Topic: import renaming?


view this post on Zulip Scott Morrison (Aug 09 2018 at 09:43):

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

view this post on Zulip Mario Carneiro (Aug 09 2018 at 09:43):

I don't think there is such a thing

view this post on Zulip 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

view this post on Zulip Patrick Massot (Aug 09 2018 at 09:44):

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

view this post on Zulip 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!

view this post on Zulip Mario Carneiro (Aug 09 2018 at 09:45):

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

view this post on Zulip Johan Commelin (Aug 09 2018 at 09:47):

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

view this post on Zulip 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