conflicting names in imports

Stream: new members

[lsnbr]

Hi, I have a small problem regarding imports and name conflicts. I need to import a file which defines a custom even and odd definition. But I also want to use some stuff from algebra.ring.basic, which when imported, also imports the library definitions of even and odd. But this is not possible in lean it seems. Cant I rename stuff on imports or only import certain names? Or how can I solve this?

[Johan Commelin]

Can you modify the custom file, to put everything in some namespace?

[Johan Commelin]

If you wrap that file in

namespace my_custom_lib

def even : ...

end my_custom_lib

then after importing, your custom def will be available as my_custom_lib.even.

[lsnbr]

I cant modify the file, only import it

[Johan Commelin]

Hmmm, I think that's a problem. Lean 4 will make this sort of stuff possible, but Lean 3 assumes that fully qualified names are unique.