Def Lean.Linter.logLintIf

Modification history

2023-11-17 05:53

Mathlib/Lean/Linter.lean

chore: bump to v4.3.0-rc2 (#8366) …

Deleted Lean.Linter.logLintIf View on Github →

2023-03-17 10:29

Mathlib/Lean/Linter.lean

feat: add logLintIf (#2933) …

Added Lean.Linter.logLintIf View on Github →