Closed rwbarton closed 1 year ago
Lots of types that started with capital letters were getting "Cat" appended even when it made no sense, e.g., Module.End, LinearMap. Here, we only add the Cat suffix when there is already a conflicting name.
Most of the names that get the Cat suffix are actually categories now. False positives: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/names.20distinguished.20only.20by.20case
Lots of types that started with capital letters were getting "Cat" appended even when it made no sense, e.g., Module.End, LinearMap. Here, we only add the Cat suffix when there is already a conflicting name.
Most of the names that get the Cat suffix are actually categories now. False positives: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/names.20distinguished.20only.20by.20case