From 2d4b7e7952a78e54fa5e11223b3231afd626559d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 27 Sep 2020 06:29:21 -0700 Subject: [PATCH] feat: add `doMatch` parser --- src/Lean/Parser/Do.lean | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/src/Lean/Parser/Do.lean b/src/Lean/Parser/Do.lean index ccae4c4493..bdf7e6aecd 100644 --- a/src/Lean/Parser/Do.lean +++ b/src/Lean/Parser/Do.lean @@ -121,7 +121,13 @@ else if c_2 then "if " >> termParser >> " then " >> doSeq >> many (checkColGe pos.column "'else if' in 'do' must be indented" >> try (" else " >> " if ") >> termParser >> " then " >> doSeq) >> optional (checkColGe pos.column "'else' in 'do' must be indented" >> " else " >> doSeq) -@[builtinDoElemParser] def doFor := parser! "for " >> termParser >> " in " >> termParser maxPrec >> doSeq +@[builtinDoElemParser] def doFor := parser! "for " >> termParser >> " in " >> termParser maxPrec >> doSeq + +/- `match`-expression where the right-hand-side of alternatives is a `doSeq` instead of a `term` -/ +def doMatchAlt : Parser := sepBy1 termParser ", " >> darrow >> doSeq +def doMatchAlts : Parser := parser! withPosition fun pos => (optional "| ") >> sepBy1 doMatchAlt (checkColGe pos.column "alternatives must be indented" >> "|") +@[builtinDoElemParser] def doMatch := parser!:leadPrec "match " >> sepBy1 matchDiscr ", " >> optType >> " with " >> doMatchAlts + @[builtinDoElemParser] def «break» := parser! "break" @[builtinDoElemParser] def «continue» := parser! "continue"