Commit 2023-01-26 14:30 702d8f3d

View on Github →

feat: add uppercase lean 3 linter (#1796)

depends on: #1794 Implements a linter for lean 3 declarations containing capital letters (as suggested on Zulip).

Estimated changes

Modified Mathlib/Algebra/EuclideanDomain/Basic.lean

Modified Mathlib/Algebra/GroupPower/Lemmas.lean

Modified Mathlib/Algebra/IndicatorFunction.lean

Modified Mathlib/Algebra/Order/LatticeGroup.lean

Modified Mathlib/Algebra/Ring/Basic.lean

Modified Mathlib/CategoryTheory/Category/KleisliCat.lean

Modified Mathlib/CategoryTheory/Category/RelCat.lean

Modified Mathlib/Combinatorics/Hall/Finite.lean

Modified Mathlib/Data/Int/GCD.lean

Modified Mathlib/Data/Nat/Factorial/Basic.lean

Modified Mathlib/Data/PFunctor/Univariate/Basic.lean

Modified Mathlib/Data/Real/Basic.lean

Modified Mathlib/Data/Real/CauSeqCompletion.lean

Modified Mathlib/Data/Seq/Computation.lean

Modified Mathlib/Data/Set/Intervals/OrdConnected.lean

Modified Mathlib/Data/Set/Sigma.lean

Modified Mathlib/Data/TypeVec.lean

Modified Mathlib/Data/W/Basic.lean

Modified Mathlib/Init/Core.lean

Modified Mathlib/Mathport/Rename.lean

added def Mathlib.Prelude.Rename.suspiciousLean3Name

Modified Mathlib/Order/Bounds/Basic.lean

Modified Mathlib/Order/Filter/AtTopBot.lean

Modified Mathlib/Order/Filter/Cofinite.lean

Modified Mathlib/Order/Filter/Pi.lean

Modified Mathlib/Order/InitialSeg.lean

Modified Mathlib/Order/LocallyFinite.lean

Modified Mathlib/Order/RelClasses.lean

Modified Mathlib/RingTheory/Coprime/Lemmas.lean

Modified Mathlib/Topology/Basic.lean