test: test missing cases error (#11107)
This PR tests the missing cases error. I thought I broke this, but it seems I did not (or at least not this way, maybe there is a way to trigger it).
This commit is contained in:
parent
d41f39fb10
commit
f843837bfa
1 changed files with 24 additions and 0 deletions
24
tests/lean/run/matchMissingCase.lean
Normal file
24
tests/lean/run/matchMissingCase.lean
Normal file
|
|
@ -0,0 +1,24 @@
|
|||
inductive Enum where | a | b | c | d
|
||||
|
||||
/--
|
||||
error: Missing cases:
|
||||
Enum.d
|
||||
Enum.c
|
||||
-/
|
||||
#guard_msgs in
|
||||
def test : Enum → Nat
|
||||
| .a => 0
|
||||
| .b => 0
|
||||
|
||||
-- set_option trace.Meta.Match.match true
|
||||
|
||||
/--
|
||||
error: Missing cases:
|
||||
Enum.d, false
|
||||
Enum.c, false
|
||||
-/
|
||||
#guard_msgs(pass trace, all) in
|
||||
def test2 : Enum → Bool → Nat
|
||||
| .a, _ => 0
|
||||
| .b, _ => 0
|
||||
| _, true => 0
|
||||
Loading…
Add table
Reference in a new issue