From f843837bfaf4fb64571ddced9fa4cdfde40c8610 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Thu, 6 Nov 2025 15:38:55 +0100 Subject: [PATCH] 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). --- tests/lean/run/matchMissingCase.lean | 24 ++++++++++++++++++++++++ 1 file changed, 24 insertions(+) create mode 100644 tests/lean/run/matchMissingCase.lean diff --git a/tests/lean/run/matchMissingCase.lean b/tests/lean/run/matchMissingCase.lean new file mode 100644 index 0000000000..36def2c81e --- /dev/null +++ b/tests/lean/run/matchMissingCase.lean @@ -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