From 2270e8cd53841b73a8e3bca57f2e2956ac1d309e Mon Sep 17 00:00:00 2001
From: Mario Carneiro <di.gama@gmail.com>
Date: Sun, 18 Sep 2022 17:00:15 -0400
Subject: [PATCH] fix: ignore unused anonymous `have` variables

---
 src/Lean/Linter/UnusedVariables.lean | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/src/Lean/Linter/UnusedVariables.lean b/src/Lean/Linter/UnusedVariables.lean
index 0766abeaa8..dea6756378 100644
--- a/src/Lean/Linter/UnusedVariables.lean
+++ b/src/Lean/Linter/UnusedVariables.lean
@@ -102,6 +102,11 @@ builtin_initialize addBuiltinUnusedVariablesIgnoreFn (fun _ stack opts =>
     (stx.isOfKind ``Lean.Parser.Term.matchAlt && pos == 1) ||
     (stx.isOfKind ``Lean.Parser.Tactic.inductionAltLHS && pos == 2))
 
+-- is anonymous have variable
+builtin_initialize addBuiltinUnusedVariablesIgnoreFn (fun stx stack _ =>
+    stx.getId == `this &&
+    (stack.matches [none, ``Lean.Parser.Term.haveIdDecl] ||
+    stack.matches [none, ``Lean.Parser.Term.haveEqnsDecl]))
 
 builtin_initialize unusedVariablesIgnoreFnsExt : SimplePersistentEnvExtension Name Unit ←
   registerSimplePersistentEnvExtension {