Def Mathlib.Linter.PPRoundtrip.ppRoundtrip

Modification history

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