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

feat(frontends/lean/builtin_exprs): make 'obtain' arguments visible by default

Browse source
This commit is contained in:
Leonardo de Moura 2015-02-05 10:38:45 -08:00
parent dfad24e3f5
commit b6dd1269b9
1 changed files with 0 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -343,15 +343,6 @@ static expr parse_obtain(parser & p, unsigned, expr const *, pos_info const & po
unsigned num_ps = ps.size(); unsigned num_ps = ps.size();
if (num_ps < 2) if (num_ps < 2)
throw parser_error("invalid 'obtain' expression, at least 2 binders expected", b_pos); throw parser_error("invalid 'obtain' expression, at least 2 binders expected", b_pos);
bool is_visible = false;
if (p.curr_is_token(get_visible_tk())) {
p.next();
is_visible = true;
}
if (!is_visible) {
expr H = ps[num_ps-1];
ps[num_ps-1] = update_local(H, mlocal_type(H), local_info(H).update_contextual(false));
}
p.check_token_next(get_comma_tk(), "invalid 'obtain' expression, ',' expected"); p.check_token_next(get_comma_tk(), "invalid 'obtain' expression, ',' expected");
p.check_token_next(get_from_tk(), "invalid 'obtain' expression, 'from' expected"); p.check_token_next(get_from_tk(), "invalid 'obtain' expression, 'from' expected");
expr H1 = p.parse_expr(); expr H1 = p.parse_expr();