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

fix(frontends/lean): name of auxiliary hypothesis in 'obtains' expression, and also marked them as non-contextual

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-07-11 04:50:53 +01:00
parent cf34f75ab5
commit 024299f56b
1 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -304,11 +304,12 @@ static expr parse_obtains(parser & p, unsigned, expr const *, pos_info const & p
p.check_token_next(g_comma, "invalid 'obtains' expression, ',' expected"); p.check_token_next(g_comma, "invalid 'obtains' expression, ',' expected");
expr b = p.parse_scoped_expr(ps, env); expr b = p.parse_scoped_expr(ps, env);
expr H = ps[num_ps-1]; expr H = ps[num_ps-1];
name H_name = local_pp_name(H);
unsigned i = num_ps-1; unsigned i = num_ps-1;
while (i > 1) { while (i > 1) {
--i; --i;
expr a = ps[i]; expr a = ps[i];
expr H_aux = mk_local(p.mk_fresh_name(), mk_expr_placeholder(), mk_contextual_info(is_fact)); expr H_aux = mk_local(p.mk_fresh_name(), H_name.append_after(i), mk_expr_placeholder(), mk_contextual_info(false));
expr H2 = Fun({a, H}, b); expr H2 = Fun({a, H}, b);
b = mk_constant(g_exists_elim)(H_aux, H2); b = mk_constant(g_exists_elim)(H_aux, H2);
H = H_aux; H = H_aux;