Mathlib Changelog
v4
Changelog
About
Github
Def
Mathlib.Linter.Style.openClassical.extractOpenNames
Modification history
2025-03-18 15:10
Mathlib/Tactic/Linter/Style.lean
feat: linter for bare `open (scoped) Classical` (#21947) …
Added
Mathlib.Linter.Style.openClassical.extractOpenNames
View on Github →