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

feat(frontends/lean): uniform unsolved goals "error" position

Browse source
This commit is contained in:
Leonardo de Moura 2014-10-20 15:52:06 -07:00
parent c09bb3cc6f
commit fd40999909
1 changed files with 5 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -154,6 +154,11 @@ static expr parse_begin_end_core(parser & p, pos_info const & pos) {
tacs.push_back(tac);
}
expr r = tacs[0];
if (tacs.size() == 1) {
// Hack: for having a uniform squiggle placement for unsolved goals.
// That is, the result is always of the form and_then(...).
r = p.mk_app({get_and_then_tac_fn(), r, get_id_tac_fn()}, end_pos);
}
for (unsigned i = 1; i < tacs.size(); i++) {
r = p.mk_app({get_and_then_tac_fn(), r, tacs[i]}, end_pos);
}