mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-25 12:42:02 +03:00
[parser] error message if use let-in in do block
This commit is contained in:
parent
26c5c4db03
commit
a01b7e25d9
@ -922,7 +922,10 @@ mutual
|
||||
<|> do decoratedKeyword fname "let"
|
||||
commit
|
||||
res <- nonEmptyBlock (letBlock fname)
|
||||
atEnd indents
|
||||
do b <- bounds (decoratedKeyword fname "in")
|
||||
fatalLoc {c = True} b.bounds "Let-in not supported in do block. Did you mean (let ... in ...)?"
|
||||
<|>
|
||||
do atEnd indents
|
||||
pure (mkDoLets fname res)
|
||||
<|> do b <- bounds (decoratedKeyword fname "rewrite" *> expr pdef fname indents)
|
||||
atEnd indents
|
||||
|
Loading…
Reference in New Issue
Block a user