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):
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