Def Mathlib.Linter.isOutside

Modification history

2025-11-18 10:56
Mathlib/Tactic/Linter/CommandStart.lean
chore: bump toolchain to v4.26.0-rc1 (#31763)
Modified Mathlib.Linter.isOutsideView on Github →
2025-06-17 18:33
Mathlib/Tactic/Linter/CommandStart.lean
feat: a linter to enforce formatting (#24465) …
Added Mathlib.Linter.isOutsideView on Github →