Commit 2023-09-12 21:07 69a3de31

View on Github →

style: a linter for colons (#6761) A linter that throws on seeing a colon at the start of a line, according to the style guideline that says these operators should go before linebreaks.

Estimated changes

modified theorem Finset.gcd_congr
modified theorem Finmap.insert_toFinmap
modified theorem Finmap.union_toFinmap
modified theorem List.Nodup.pairwise_coe
modified theorem StrictMonoOn.le_iff_le
modified def Lean.Expr.app7?