diff --git a/src/Lean/Elab/Match.lean b/src/Lean/Elab/Match.lean index fdbe7a6c6b3a..48a2cd6a604d 100644 --- 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 index 96a2633f3ede..51ed5b736a11 100644 --- 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'