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

feat(frontends/lean/builtin_exprs): focus on have-tactic goal

Browse source
This commit is contained in:
Leonardo de Moura 2015-03-01 13:43:33 -08:00
parent e07c6675b3
commit c8ad5e9406
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/builtin_exprs.cpp
View file

@ -204,6 +204,8 @@ static expr parse_begin_end_core(parser & p, pos_info const & pos, name const &
auto pos = p.pos();
expr t = p.parse_expr();
t = p.mk_app(get_exact_tac_fn(), t, pos);
t = p.save_pos(mk_begin_end_element_annotation(t), pos);
t = p.save_pos(mk_begin_end_annotation(t), pos);
add_tac(t, pos);
} else if (p.curr_is_token(get_proof_tk())) {
auto pos = p.pos();
@ -211,6 +213,8 @@ static expr parse_begin_end_core(parser & p, pos_info const & pos, name const &
expr t = p.parse_expr();
p.check_token_next(get_qed_tk(), "invalid proof-qed, 'qed' expected");
t = p.mk_app(get_exact_tac_fn(), t, pos);
t = p.save_pos(mk_begin_end_element_annotation(t), pos);
t = p.save_pos(mk_begin_end_annotation(t), pos);
add_tac(t, pos);
} else if (p.curr_is_token(get_begin_tk())) {
auto pos = p.pos();