perf: unused variables linter: early cut-off

This commit is contained in:
Sebastian Ullrich 2022-07-28 15:20:26 +02:00 committed by Leonardo de Moura
parent 2a977d8969
commit e048bbc93a

View file

@ -151,6 +151,9 @@ opaque getUnusedVariablesIgnoreFns : CommandElabM (Array IgnoreFunction)
def unusedVariables : Linter := fun cmdStx => do
unless getLinterUnusedVariables (← getOptions) do
return
-- NOTE: `messages` is local to the current command
if (← get).messages.hasErrors then
return