From b2a8f4118d7fb88610f3c13452a55c6246e79835 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 1 Jan 2014 14:46:19 -0800 Subject: [PATCH] feat(library/elaborator): process ho-match before normalizing Signed-off-by: Leonardo de Moura --- src/library/elaborator/elaborator.cpp | 2 +- tests/lean/subst.lean.expected.out | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/library/elaborator/elaborator.cpp b/src/library/elaborator/elaborator.cpp index c1f02297d..bd6ce6815 100644 --- a/src/library/elaborator/elaborator.cpp +++ b/src/library/elaborator/elaborator.cpp @@ -1318,7 +1318,7 @@ class elaborator::imp { r = process_metavar(c, b, a, false); if (r != Continue) { return r == Processed; } - if (normalize_head(a, b, c)) { return true; } + if (!is_meta_app(a) && !is_meta_app(b) && normalize_head(a, b, c)) { return true; } if (!eq) { // TODO(Leo): use is_actual_lower and is_actual_upper diff --git a/tests/lean/subst.lean.expected.out b/tests/lean/subst.lean.expected.out index bb72e80d7..846790642 100644 --- a/tests/lean/subst.lean.expected.out +++ b/tests/lean/subst.lean.expected.out @@ -10,4 +10,4 @@ Set: lean::pp::notation Set: lean::pp::implicit Theorem T : @eq ℤ (Int::add (Int::add a (nat_to_int n)) a) (nat_to_int 10) := - @Subst ℤ a (nat_to_int n) (λ x : ℤ, Int::add (Int::add a x) a == nat_to_int 10) H1 H2 + @Subst ℤ a (nat_to_int n) (λ x : ℤ, @eq ℤ (Int::add (Int::add a x) a) (nat_to_int 10)) H1 H2