From d011c00010429728fab0bb3675b13f4bce63539e Mon Sep 17 00:00:00 2001
From: Kyle Miller <kmill31415@gmail.com>
Date: Wed, 16 Oct 2024 21:29:16 -0700
Subject: [PATCH] fix: make `proof_wanted` not report unused variables (#997)

---
 Batteries/Util/ProofWanted.lean |  9 ++++++---
 test/proof_wanted.lean          | 15 +++++++++++++++
 2 files changed, 21 insertions(+), 3 deletions(-)
 create mode 100644 test/proof_wanted.lean

diff --git a/Batteries/Util/ProofWanted.lean b/Batteries/Util/ProofWanted.lean
index 97f1473f70..3a6fd90981 100644
--- a/Batteries/Util/ProofWanted.lean
+++ b/Batteries/Util/ProofWanted.lean
@@ -33,7 +33,10 @@ elaboration, but it's then removed from the environment.
 def elabProofWanted : CommandElab
   | `($mods:declModifiers proof_wanted $name $args* : $res) => withoutModifyingEnv do
     -- The helper axiom is used instead of `sorry` to avoid spurious warnings
-    elabCommand <| ← `(axiom helper (p : Prop) : p
-                       $mods:declModifiers
-                       theorem $name $args* : $res := helper _)
+    elabCommand <| ← `(
+      section
+      set_option linter.unusedVariables false
+      axiom helper {α : Sort _} : α
+      $mods:declModifiers theorem $name $args* : $res := helper
+      end)
   | _ => throwUnsupportedSyntax
diff --git a/test/proof_wanted.lean b/test/proof_wanted.lean
new file mode 100644
index 0000000000..38f5714eb3
--- /dev/null
+++ b/test/proof_wanted.lean
@@ -0,0 +1,15 @@
+import Batteries.Util.ProofWanted
+
+/-!
+No unused variable warnings.
+-/
+#guard_msgs in proof_wanted foo (x : Nat) : True
+
+/-!
+When not a proposition, rely on `theorem` command failing.
+-/
+/--
+error: type of theorem 'foo' is not a proposition
+  Nat → Nat
+-/
+#guard_msgs in proof_wanted foo (x : Nat) : Nat