Renaming in root?

Stream: lean4

[François G. Dorais]

Is it possible to rename declarations in the root namespace? open _root_ renaming ... doesn't work. My current workaround is to define abbreviations instead but that's not quite the same.

[Mac]

My understanding is the answer is no.

[Mac]

However, if all you care about is literally using a different name/notation for something in some local scope, you could do some like this though:

local notation "id'" => id
#check id' -- maps to `id` (and even is now printed as `id'`)