max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: match_expr parser (#4007)

Browse source 
closes #3989
closes #3990
This commit is contained in:
Leonardo de Moura 2024-04-28 01:56:28 +02:00 • committed by GitHub
parent a359586a96
commit 8fa36c7730
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
5 changed files with 13 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/Parser/Term.lean
View file

@ -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)

3
tests/lean/3989_1.lean Normal file
View file

@ -0,0 +1,3 @@
def foo (ty : Expr) : MetaM Expr :=
match_expr ty with
| Nat => sorry

1
tests/lean/3989_1.lean.expected.out Normal file
View file

@ -0,0 +1 @@
3989_1.lean:4:0: error: expected else-alternative for `match_expr`, i.e., `| _ => ...`

6
tests/lean/3989_2.lean Normal file
View file

@ -0,0 +1,6 @@
def foo (ty : Expr) : MetaM Expr :=
match_expr ty with
| Nat => sorry
| BitVec n => sorry
#check Nat

2
tests/lean/3989_2.lean.expected.out Normal file
View file

@ -0,0 +1,2 @@
3989_2.lean:6:0: error: expected else-alternative for `match_expr`, i.e., `| _ => ...`
Nat : Type