From 94549fdf12a38a93ef8960ac0e286363ffb03c62 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 13 Sep 2024 11:20:07 +0200 Subject: [PATCH] fix: inaccessible pattern vars reported as binders --- src/Lean/Elab/Match.lean | 2 +- tests/lean/linterUnusedVariables.lean | 7 +++++++ 2 files changed, 8 insertions(+), 1 deletion(-) 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 aa285db063d9..3640b533ad9d 100644 --- a/tests/lean/linterUnusedVariables.lean +++ b/tests/lean/linterUnusedVariables.lean @@ -255,3 +255,10 @@ def ignoreEverything : Lean.Linter.IgnoreFunction := fun _ _ _ => true def ignored (x : Nat) := 0 + +/-! +The wildcard pattern introduces a copy of `x` that should not be linted as it is in an +inaccessible annotation. +-/ +example : (x = y) → y = x + | .refl _ => .refl _