Mathlib Changelog
v4
Changelog
About
Github
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