Commit 2025-02-10 10:42 887c81f2

View on Github →

feat: lint declarations which contain a double underscore (#17580)

Estimated changes

Modified Mathlib/ModelTheory/PartialEquiv.lean

deleted theorem FirstOrder.Language.PartialEquiv.toEmbeddingOfEqTop__apply

added theorem FirstOrder.Language.PartialEquiv.toEmbeddingOfEqTop_apply

Modified Mathlib/Tactic/Linter/Style.lean

added def Mathlib.Linter.Style.nameCheck.doubleUnderscore:

Created MathlibTest/DoubleUnderscore.lean

added def double__underscore

Modified MathlibTest/Lint.lean

added theorem double__underscore