diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean index 6ffe3e4be7..e71e7788bb 100644 --- a/src/Lean/Parser/Term.lean +++ b/src/Lean/Parser/Term.lean @@ -870,7 +870,7 @@ def matchExprElseAlt (rhsParser : Parser) := leading_parser "| " >> ppIndent (ho def matchExprAlts (rhsParser : Parser) := leading_parser withPosition $ many (ppLine >> checkColGe "irrelevant" >> notFollowedBy (symbol "| " >> " _ ") "irrelevant" >> matchExprAlt rhsParser) - >> (ppLine >> checkColGe "irrelevant" >> matchExprElseAlt rhsParser) + >> (ppLine >> checkColGe "else-alternative for `match_expr`, i.e., `| _ => ...`" >> matchExprElseAlt rhsParser) @[builtin_term_parser] def matchExpr := leading_parser:leadPrec "match_expr " >> termParser >> " with" >> ppDedent (matchExprAlts termParser) diff --git a/tests/lean/3989_1.lean b/tests/lean/3989_1.lean new file mode 100644 index 0000000000..adbbfb2f42 --- /dev/null +++ b/tests/lean/3989_1.lean @@ -0,0 +1,3 @@ +def foo (ty : Expr) : MetaM Expr := + match_expr ty with + | Nat => sorry diff --git a/tests/lean/3989_1.lean.expected.out b/tests/lean/3989_1.lean.expected.out new file mode 100644 index 0000000000..188b2bb20a --- /dev/null +++ b/tests/lean/3989_1.lean.expected.out @@ -0,0 +1 @@ +3989_1.lean:4:0: error: expected else-alternative for `match_expr`, i.e., `| _ => ...` diff --git a/tests/lean/3989_2.lean b/tests/lean/3989_2.lean new file mode 100644 index 0000000000..962415b0c1 --- /dev/null +++ b/tests/lean/3989_2.lean @@ -0,0 +1,6 @@ +def foo (ty : Expr) : MetaM Expr := + match_expr ty with + | Nat => sorry + | BitVec n => sorry + +#check Nat diff --git a/tests/lean/3989_2.lean.expected.out b/tests/lean/3989_2.lean.expected.out new file mode 100644 index 0000000000..4e1569eb91 --- /dev/null +++ b/tests/lean/3989_2.lean.expected.out @@ -0,0 +1,2 @@ +3989_2.lean:6:0: error: expected else-alternative for `match_expr`, i.e., `| _ => ...` +Nat : Type