fix: inaccessible pattern vars reported as binders

leanprover · Sep 13, 2024 · c5747f1 · c5747f1
1 parent 79943be
commit c5747f1
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 1 deletion.
diff --git a/src/Lean/Elab/Match.lean b/src/Lean/Elab/Match.lean
@@ -643,7 +643,7 @@ where
     | .proj _ _ b       => return p.updateProj! (← go b)
     | .mdata k b        =>
       if inaccessible? p |>.isSome then
-        return mkMData k (← withReader (fun _ => false) (go b))
+        return mkMData k (← withReader (fun _ => true) (go b))
       else if let some (stx, p) := patternWithRef? p then
         Elab.withInfoContext' (go p) fun p => do
           /- If `p` is a free variable and we are not inside of an "inaccessible" pattern, this `p` is a binder. -/

diff --git a/tests/lean/linterUnusedVariables.lean b/tests/lean/linterUnusedVariables.lean
@@ -266,3 +266,7 @@ def A.out : A → Nat
 theorem problematicAlias (n : A) (i : Nat) (h : i ≤ n.out) : i ≤ n.out :=
   match n with
   | .intro _ => by assumption
+
+example : (x = y) → y = x
+  | .refl _ => .refl _
+        --^ unused variable 'x'