linter

leanprover · Dec 31, 2024 · dd9ad37 · dd9ad37
1 parent 649b2a9
commit dd9ad37
Showing 1 changed file with 1 addition and 0 deletions.
diff --git 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 _} : α