Def Mathlib.Linter.capSourceInfo

Modification history

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