Def Mathlib.Linter.zoomString

Modification history

2025-11-18 10:56

Mathlib/Tactic/Linter/PPRoundtrip.lean

chore: bump toolchain to v4.26.0-rc1 (#31763)

Modified Mathlib.Linter.zoomString View on Github →

2024-10-08 09:48

Mathlib/Tactic/Linter/PPRoundtrip.lean

feat(Tactic/Linter): the ppRoundtrip linter (#15535) …

Added Mathlib.Linter.zoomString View on Github →