Def Mathlib.Linter.Style.openClassical.openClassicalLinter

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.openClassicalLinter View on Github →