Yeah but if you don't keep tabs on it, you might not know what to prompt it to fix. For example, early on I established in my fun proof assistant project, that I did NOT want total functions (1/0 should not be permitted, 3-4 not permitted in N), and it seems to have forgotten that along the way and it took a 2 day struggle session to remove total functions from the standard library.

Managed to get it in time to have an accurate claim that "stdlib has no total functions" prior to presenting it to someone semifamous, who doesn't like that lean has total functions