Def Mathlib.Linter.polishPP

Modification history

2024-10-08 09:48
Mathlib/Tactic/Linter/PPRoundtrip.lean
feat(Tactic/Linter): the ppRoundtrip linter (#15535) …
Added Mathlib.Linter.polishPPView on Github →