fix: make proof_wanted not report unused variables (#997)

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

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