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

fix(frontends/lean/frontend_elaborator): must elaborate type attached to placeholder, it may also contain holes

Browse source 
The test tactic14.lean exposes the problem.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-12-07 15:37:54 -08:00
parent b6b520302d
commit 1ff6013594
3 changed files with 18 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/frontends/lean/frontend_elaborator.cpp
View file

@ -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 {

12
tests/lean/tactic14.lean Normal file
View file

@ -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.

5
tests/lean/tactic14.lean.expected.out Normal file
View file

@ -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)