Day 1, I defined a type foo
and a function bar
:
Variant foo := A | B.
Definition bar (x : foo) : bool :=
match x with
| A => true
| B => false
end.
Day 2, I modified type foo
:
Variant foo := A | C | D.
but forgot to update bar
accordingly. However, bar
still compiles—it treated B
as a wildcard rather than constructor.
Is there an equivalent to “unused parameter” warning for Coq? If no, is it worth adding such warning and suggest replacing pattern B
with _
?