michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(frontends/lean/builtin_exprs): 'using' expression

Browse source
This commit is contained in:
Leonardo de Moura 2016-02-29 13:23:39 -08:00
parent faa0031d4e
commit bf60999ede
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -339,7 +339,7 @@ static expr parse_using_expr(parser & p, pos_info const & using_pos) {
auto id_pos = p.pos(); auto id_pos = p.pos();
expr l = p.parse_id(); expr l = p.parse_id();
if (!is_local(l)) if (!is_local(l))
throw parser_error("invalid 'using' declaration for 'have', local expected", id_pos); throw parser_error("invalid 'using' declaration, local expected", id_pos);
expr new_l; expr new_l;
binder_info bi = local_info(l); binder_info bi = local_info(l);
if (p.is_local_variable_parameter(local_pp_name(l))) { if (p.is_local_variable_parameter(local_pp_name(l))) {
@ -353,7 +353,7 @@ static expr parse_using_expr(parser & p, pos_info const & using_pos) {
new_locals.push_back(new_l); new_locals.push_back(new_l);
} }
p.next(); // consume ',' p.next(); // consume ','
expr pr = parse_proof(p); expr pr = p.parse_expr();
unsigned i = locals.size(); unsigned i = locals.size();
while (i > 0) { while (i > 0) {
--i; --i;