Mathlib v3 is deprecated. Go to Mathlib v4

Inductive lint_verbosity

Modification history

2020-07-29 11:45

src/tactic/lint/frontend.lean

feat(tactic/lint): quieter output by default (#3622) …

Added lint_verbosity View on Github →