From dd9ad37716eabfa0c0555092ffc5a4ac8f233a13 Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Tue, 31 Dec 2024 14:28:41 -0500 Subject: [PATCH] linter --- tests/lean/run/extract_lets.lean | 1 + 1 file changed, 1 insertion(+) 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 _} : α