Commit 2023-08-10 12:07 65a35f78

View on Github →

chore: ensure all instances referred to directly have explicit names (#6423) Per https://github.com/leanprover/lean4/issues/2343, we are going to need to change the automatic generation of instance names, as they become too long. This PR ensures that everywhere in Mathlib that refers to an instance by name, that name is given explicitly, rather than being automatically generated. There are four exceptions, which are now commented, with links to https://github.com/leanprover/lean4/issues/2343. This was implemented by running Mathlib against a modified Lean that appended _ᾰ to all automatically generated names, and fixing everything.

Estimated changes