max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: reword redundant alternative error explanation (#9001)

Browse source 
This PR adjusts the `lean.redundantMatchAlt` error explanation to remove
the word "unprefixed," which the reference manual's style linter does
not recognize.
This commit is contained in:
jrr6 2025-06-25 18:15:22 -04:00 • committed by GitHub
parent 25b1b46572
commit 8da2f7105c
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/Lean/ErrorExplanations/RedundantMatchAlt.lean
View file

@ -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