diff --git a/tests/lean/run/extract_lets.lean b/tests/lean/run/extract_lets.lean index e8ba7293e785..d450af9da010 100644 --- a/tests/lean/run/extract_lets.lean +++ b/tests/lean/run/extract_lets.lean @@ -2,6 +2,7 @@ # Tests of the `extract_lets` tactic -/ +set_option linter.tactic.unusedName true set_option linter.unusedVariables false axiom test_sorry {α : Sort _} : α