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

fix: { ... : <expected-type> } syntax in the old frontend

Browse source
This commit is contained in:
Leonardo de Moura 2020-05-20 15:49:40 -07:00
parent 05dda45a22
commit c01da783ca
1 changed files with 4 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/frontends/lean/brackets.cpp
View file

@ -82,6 +82,8 @@ static expr parse_structure_instance_core(parser & p, optional<expr> const & src
p.next();
catchall = true;
break;
} else if (p.curr_is_token(get_colon_tk())) {
break;
} else if (!read_source) {
fns.push_back(p.check_id_next("invalid structure instance, identifier expected"));
p.check_token_next(get_assign_tk(), "invalid structure instance, ':=' expected");
@ -176,6 +178,8 @@ expr parse_curly_bracket(parser & p, unsigned, expr const *, pos_info const & po
return p.save_pos(mk_structure_instance(), pos);
} else if (p.curr_is_token(get_dotdot_tk())) {
return parse_structure_instance_core(p);
} else if (p.curr_is_token(get_colon_tk())) {
return parse_structure_instance_core(p);
} else {
e = p.parse_expr();
}