Commit 2025-02-16 09:19 1d9f57a8

View on Github →

feat: rewrite the linter for spaces before semicolons in Lean (#16532) A fix about 30 violations which have crept into mathlib in the mean-time.

Estimated changes

Modified Mathlib/AlgebraicTopology/SimplicialSet/Coskeletal.lean

Modified Mathlib/CategoryTheory/Comma/CardinalArrow.lean

Modified Mathlib/Combinatorics/Quiver/ReflQuiver.lean

Modified Mathlib/Probability/CondVar.lean

modified theorem ProbabilityTheory.condVar_congr_ae

modified theorem ProbabilityTheory.condVar_const

modified theorem ProbabilityTheory.condVar_neg

modified theorem ProbabilityTheory.condVar_of_not_le

modified theorem ProbabilityTheory.condVar_smul

modified theorem ProbabilityTheory.condVar_zero

modified theorem ProbabilityTheory.integrable_condVar

modified theorem ProbabilityTheory.stronglyMeasurable_condVar

Modified Mathlib/Probability/Variance.lean

modified theorem ProbabilityTheory.variance_eq_integral

Modified Mathlib/Tactic/Linter/TextBased.lean

added def Mathlib.Linter.TextBased.semicolonLinter

Modified scripts/lint-style.py