diff --git a/src/Lean/Parser/Do.lean b/src/Lean/Parser/Do.lean index 9b58c64405..2e57b334a8 100644 --- a/src/Lean/Parser/Do.lean +++ b/src/Lean/Parser/Do.lean @@ -109,12 +109,18 @@ def doFinally := leading_parser "finally " >> doSeq @[builtinDoElemParser] def doAssert := leading_parser:leadPrec "assert! " >> termParser /- -We use `notFollowedBy` to avoid counterintuitive behavior. For example, the `if`-term parser +We use `notFollowedBy` to avoid counterintuitive behavior. + +For example, the `if`-term parser doesn't enforce indentation restrictions, but we don't want it to be used when `doIf` fails. Note that parser priorities would not solve this problem since the `doIf` parser is failing while the `if` -parser is succeeding. +parser is succeeding. The first `notFollowedBy` prevents this problem. + +Consider the `doElem` `x := (a, b⟩` it contains an error since we are using `⟩` instead of `)`. Thus, `doReassign` parser fails. +However, `doExpr` would succeed consuming just `x`, and cryptic error message is generated after that. +The second `notFollowedBy` prevents this problem. -/ -@[builtinDoElemParser] def doExpr := leading_parser notFollowedByRedefinedTermToken >> termParser +@[builtinDoElemParser] def doExpr := leading_parser notFollowedByRedefinedTermToken >> termParser >> notFollowedBy (symbol ":=" <|> symbol "←" <|> symbol "<-") "unexpected token after 'expr' in 'do' block" @[builtinDoElemParser] def doNested := leading_parser "do " >> doSeq @[builtinTermParser] def «do» := leading_parser:maxPrec "do " >> doSeq diff --git a/tests/lean/348.lean b/tests/lean/348.lean new file mode 100644 index 0000000000..0aa2fd72f1 --- /dev/null +++ b/tests/lean/348.lean @@ -0,0 +1,4 @@ +def doSomething (db:String) : String := do + let mut cl : Nat × Nat → Nat × Nat := λx => x + cl := (λ(x,y) => (x, y⟩) + db diff --git a/tests/lean/348.lean.expected.out b/tests/lean/348.lean.expected.out new file mode 100644 index 0000000000..4abed64a94 --- /dev/null +++ b/tests/lean/348.lean.expected.out @@ -0,0 +1 @@ +348.lean:3:24: error: expected ')'