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

feat(frontends/lean/builtin_exprs): add optional curly braces for do-notation

Browse source
This commit is contained in:
Leonardo de Moura 2016-05-25 15:15:39 -07:00
parent 2a16b58324
commit 7c97d88be5
1 changed files with 8 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/frontends/lean/builtin_exprs.cpp
View file

@ -518,6 +518,11 @@ static expr parse_do(parser & p, unsigned, expr const *, pos_info const & pos) {
parser::local_scope scope(p);
buffer<expr> es;
buffer<expr> locals;
bool has_braces = false;
if (p.curr_is_token(get_lcurly_tk())) {
has_braces = true;
p.next();
}
while (true) {
expr curr;
optional<name> id;
@ -555,6 +560,9 @@ static expr parse_do(parser & p, unsigned, expr const *, pos_info const & pos) {
break;
}
}
if (has_braces) {
p.check_token_next(get_rcurly_tk(), "invalid 'do' expression, '}' expected");
}
lean_assert(!es.empty());
lean_assert(es.size() == locals.size() + 1);
if (es.size() == 1)