Reinventig the wheel

Stream: new members

[capli]

I find it helpful when learning a new tool, to re-write already existing material, to go through and see how each element interacts, etc. Is there a way to disable lean's library to mitigate name collisions, and/or reliance on already existing code, or does lean become essentially unusable in such a state?

[Johan Commelin]

@capli depends on how far you want to go. You can certainly avoid using mathlib. If you also want to avoid the core library, you should start your files with prelude. And yes, lean will not be very usable. But that seems to be what you want (-;

[capli]

@Johan Commelin Well, depending on the meaning of "useable", yes. hahaha
Thank you for the tip!

[Kevin Buzzard]

I've done a fair bit of this sort of thing when learning and teaching Lean. For example I rewrote data.complex.basic and here there were no issues -- I just didn't import data.complex.basic. But some students and I rewrote basic group theory whilst having group theory already imported and here it was more of a pain. We spend our entire time in the mygroup namespace and even then things don't always go smoothly, because there are lemmas about groups which live in the root namespace so one inevitably gets collisions; we just made do with writing mygroup.blah now and again, and having mygroup.group open.