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

feat(library/elaborator): process ho-match before normalizing

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-01-01 14:46:19 -08:00
parent a299778c88
commit b2a8f4118d
2 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/library/elaborator/elaborator.cpp
View file

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

2
tests/lean/subst.lean.expected.out
View file

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