From 8da2f7105cd454e809f4e961e157d5281a52215c Mon Sep 17 00:00:00 2001
From: jrr6 <7482866+jrr6@users.noreply.github.com>
Date: Wed, 25 Jun 2025 18:15:22 -0400
Subject: [PATCH] chore: reword redundant alternative error explanation (#9001)

This PR adjusts the `lean.redundantMatchAlt` error explanation to remove
the word "unprefixed," which the reference manual's style linter does
not recognize.
---
 src/Lean/ErrorExplanations/RedundantMatchAlt.lean | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/Lean/ErrorExplanations/RedundantMatchAlt.lean b/src/Lean/ErrorExplanations/RedundantMatchAlt.lean
index 80abf0bf0a..4af781a4ce 100644
--- a/src/Lean/ErrorExplanations/RedundantMatchAlt.lean
+++ b/src/Lean/ErrorExplanations/RedundantMatchAlt.lean
@@ -24,10 +24,10 @@ specified, this error indicates that the specified pattern will always be matche
 binding in question can be replaced with a standard pattern-matching `let`.
 
 One common cause of this error is that a pattern that was intended to match a constructor was
-instead interpreted as a variable binding. This occurs, for instance, if an unprefixed constructor
-name (e.g., `cons`) is used outside of its namespace (`List`). The constructor-name-as-variable
-linter, enabled by default, will display a warning on any variable patterns that resemble
-constructor names.
+instead interpreted as a variable binding. This occurs, for instance, if a constructor
+name (e.g., `cons`) is written without its prefix (`List`) outside of that type's namespace. The
+constructor-name-as-variable linter, enabled by default, will display a warning on any variable
+patterns that resemble constructor names.
 
 This error nearly always indicates an issue with the code where it appears. If needed, however,
 `set_option match.ignoreUnusedAlts true` will disable the check for this error and allow pattern