From 024299f56b31c0157dd2caf79359c76d6be919fe Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 11 Jul 2014 04:50:53 +0100 Subject: [PATCH] fix(frontends/lean): name of auxiliary hypothesis in 'obtains' expression, and also marked them as non-contextual Signed-off-by: Leonardo de Moura --- src/frontends/lean/builtin_exprs.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp index 4f0399ba7..8f9f97ef9 100644 --- a/src/frontends/lean/builtin_exprs.cpp +++ b/src/frontends/lean/builtin_exprs.cpp @@ -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"); expr b = p.parse_scoped_expr(ps, env); expr H = ps[num_ps-1]; + name H_name = local_pp_name(H); unsigned i = num_ps-1; while (i > 1) { --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); b = mk_constant(g_exists_elim)(H_aux, H2); H = H_aux;