From 1ff6013594025bef810360268bae08ba80cf82e1 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 7 Dec 2013 15:37:54 -0800 Subject: [PATCH] fix(frontends/lean/frontend_elaborator): must elaborate type attached to placeholder, it may also contain holes The test tactic14.lean exposes the problem. Signed-off-by: Leonardo de Moura --- src/frontends/lean/frontend_elaborator.cpp | 2 +- tests/lean/tactic14.lean | 12 ++++++++++++ tests/lean/tactic14.lean.expected.out | 5 +++++ 3 files changed, 18 insertions(+), 1 deletion(-) create mode 100644 tests/lean/tactic14.lean create mode 100644 tests/lean/tactic14.lean.expected.out diff --git a/src/frontends/lean/frontend_elaborator.cpp b/src/frontends/lean/frontend_elaborator.cpp index 13e3de263..db6bd41af 100644 --- a/src/frontends/lean/frontend_elaborator.cpp +++ b/src/frontends/lean/frontend_elaborator.cpp @@ -123,7 +123,7 @@ class frontend_elaborator::imp { virtual expr visit_constant(expr const & e, context const & ctx) { if (is_placeholder(e)) { - expr m = m_ref.m_menv.mk_metavar(ctx, const_type(e)); + expr m = m_ref.m_menv.mk_metavar(ctx, visit(const_type(e), ctx)); m_ref.m_trace[m] = e; return m; } else { diff --git a/tests/lean/tactic14.lean b/tests/lean/tactic14.lean new file mode 100644 index 000000000..9d7eb5de4 --- /dev/null +++ b/tests/lean/tactic14.lean @@ -0,0 +1,12 @@ +(** + +-- Tactic for trying to prove goal using Reflexivity, Congruence and available assumptions +congr_tac = TRY(unfold_tac("eq")) ..REPEAT(ORELSE(apply_tac("Refl"), apply_tac("Congr"), assumption_tac)) + +**) + +Theorem T1 (a b : Int) (f : Int -> Int) : a = b -> (f (f a)) = (f (f b)) := + fun assumption : a = b, + show (f (f a)) = (f (f b)) by congr_tac + +Show Environment 1. diff --git a/tests/lean/tactic14.lean.expected.out b/tests/lean/tactic14.lean.expected.out new file mode 100644 index 000000000..7d2bbaf73 --- /dev/null +++ b/tests/lean/tactic14.lean.expected.out @@ -0,0 +1,5 @@ + Set: pp::colors + Set: pp::unicode + Proved: T1 +Theorem T1 (a b : ℤ) (f : ℤ → ℤ) (assumption : a = b) : (f (f a)) = (f (f b)) := + Congr (Refl f) (Congr (Refl f) assumption)