Commit 2026-01-31 13:23 eed54db1
View on Github →perf(Linter/Whitespace): revert #26240 (#34645) This causes significant regressions to code with many violations, see e.g. https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/.60linear_combination.60.20performance.20regression.20in.20v4.2E28.2E0-rc1. Going from srcNat := ls.length to srcNat := ls.positions.count causes a regression, as this could go through the string linearly. Let us revert this change instead; it is not forward-compatible with #30658 anyway.