About: redundantMatchAlt
This error occurs when an alternative in a pattern match can never be reached: any values that would match the provided patterns would also match some preceding alternative. Refer to the Pattern Matching manual section for additional details about pattern matching.
This error may appear in any pattern matching expression, including
Lean.Parser.Term.match : termPattern matching. `match e, ... with | p, ... => f | ...` matches each given
term `e` against each pattern `p` of a match alternative. When all patterns
of an alternative match, the `match` term evaluates to the value of the
corresponding right-hand side `f` with the pattern variables bound to the
respective matched values.
If used as `match h : e, ... with | p, ... => f | ...`, `h : e = p` is available
within `f`.
When not constructing a proof, `match` does not automatically substitute variables
matched on in dependent variables' types. Use `match (generalizing := true) ...` to
enforce this.
Syntax quotations can also be used in a pattern match.
This matches a `Syntax` value against quotations, pattern variables, or `_`.
Quoted identifiers only match identical identifiers - custom matching such as by the preresolved
names only should be done explicitly.
`Syntax.atom`s are ignored during matching by default except when part of a built-in literal.
For users introducing new atoms, we recommend wrapping them in dedicated syntax kinds if they
should participate in matching.
For example, in
```lean
syntax "c" ("foo" <|> "bar") ...
```
`foo` and `bar` are indistinguishable during matching, but in
```lean
syntax foo := "foo"
syntax "c" (foo <|> "bar") ...
```
they are not.
match expressions, equational function definitions, if let
bindings, and monadic Lean.Parser.Term.let : term`let` is used to declare a local definition. Example:
```
let x := 1
let y := x + 1
x + y
```
Since functions are first class citizens in Lean, you can use `let` to declare
local functions too.
```
let double := fun x => 2*x
double (double 3)
```
For recursive definitions, you should use `let rec`.
You can also perform pattern matching using `let`. For example,
assume `p` has type `Nat × Nat`, then you can write
```
let (x, y) := p
x + y
```
The *anaphoric let* `let := v` defines a variable called `this`.
let bindings with fallback clauses.
In pattern-matches with multiple arms, this error may occur if a less-specific pattern precedes a more-specific one that it subsumes. Bear in mind that expressions are matched against patterns from top to bottom, so specific patterns should precede generic ones.
In termIfLet : term`if let pat := d then t else e` is a shorthand syntax for:
```
match d with
| pat => t
| _ => e
```
It matches `d` against the pattern `pat` and the bindings are available in `t`.
If the pattern does not match, it returns `e` instead.
if let bindings and monadic Lean.Parser.Term.let : term`let` is used to declare a local definition. Example:
```
let x := 1
let y := x + 1
x + y
```
Since functions are first class citizens in Lean, you can use `let` to declare
local functions too.
```
let double := fun x => 2*x
double (double 3)
```
For recursive definitions, you should use `let rec`.
You can also perform pattern matching using `let`. For example,
assume `p` has type `Nat × Nat`, then you can write
```
let (x, y) := p
x + y
```
The *anaphoric let* `let := v` defines a variable called `this`.
let bindings with fallback
clauses, in which only one pattern is specified, this error indicates that the specified pattern
will always be matched. In this case, the binding in question can be replaced with a standard
pattern-matching Lean.Parser.Term.let : term`let` is used to declare a local definition. Example:
```
let x := 1
let y := x + 1
x + y
```
Since functions are first class citizens in Lean, you can use `let` to declare
local functions too.
```
let double := fun x => 2*x
double (double 3)
```
For recursive definitions, you should use `let rec`.
You can also perform pattern matching using `let`. For example,
assume `p` has type `Nat × Nat`, then you can write
```
let (x, y) := p
x + y
```
The *anaphoric let* `let := v` defines a variable called `this`.
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 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
matches with redundant alternatives to be compiled by discarding the unused arms.
Examples
Incorrect Ordering of Pattern Matches
Since any expression matching (_ :: x :: _) :: xss will also match _ :: xss, the last
alternative in the broken implementation is never reached. We resolve this by moving the more
specific alternative before the more general one.
Unnecessary Fallback Clause
Here, the fallback clause serves as a catch-all for all values of p that do not match (m, n).
However, no such values exist, so the fallback clause is unnecessary and can be removed. A similar
error arises when using if let pat := e when e will always match pat.
Pattern Treated as Variable, Not Constructor
In the original example, nil is treated as a variable, not as a constructor name, since this
definition is not within the List namespace. Thus, all values of xs will match the first
pattern, rendering the second unused. Notice that the constructor-name-as-variable linter displays a
warning at nil, indicating its similarity to a valid constructor name. Using dot-prefix notation,
as shown in the fixed example, or specifying the full constructor name List.nil
achieves the intended behavior.