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

fix(frontends/lean/builtin_exprs): 'using' expression should make local constant available for tactics

Browse source
This commit is contained in:
Leonardo de Moura 2015-02-08 17:27:22 -08:00
parent fcd67649ed
commit 666f697d24
1 changed files with 10 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -233,21 +233,28 @@ static expr parse_proof(parser & p, expr const & prop) {
p.next(); p.next();
parser::local_scope scope(p); parser::local_scope scope(p);
buffer<expr> locals; buffer<expr> locals;
buffer<expr> new_locals;
while (!p.curr_is_token(get_comma_tk())) { while (!p.curr_is_token(get_comma_tk())) {
auto id_pos = p.pos(); auto id_pos = p.pos();
expr l = p.parse_expr(); expr l = p.parse_expr();
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 for 'have', local expected", id_pos);
p.add_local(l); expr new_l = l;
binder_info bi = local_info(l);
if (!bi.is_contextual())
new_l = update_local(l, bi.update_contextual(true));
p.add_local(new_l);
locals.push_back(l); locals.push_back(l);
new_locals.push_back(new_l);
} }
p.next(); // consume ',' p.next(); // consume ','
expr pr = parse_proof(p, prop); expr pr = parse_proof(p, prop);
unsigned i = locals.size(); unsigned i = locals.size();
while (i > 0) { while (i > 0) {
--i; --i;
expr l = locals[i]; expr l = locals[i];
pr = p.save_pos(Fun(l, pr), using_pos); expr new_l = new_locals[i];
pr = p.save_pos(Fun(new_l, pr), using_pos);
pr = p.save_pos(mk_app(pr, l), using_pos); pr = p.save_pos(mk_app(pr, l), using_pos);
} }
return pr; return pr;