From 1dedd2829c73fbc254a1d22d86db8a74080603d6 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 14 May 2015 18:21:17 -0700 Subject: [PATCH] fix(library/match): bug in higher-order matcher --- src/library/match.cpp | 2 -- tests/lua/hop1.lua | 2 +- 2 files changed, 1 insertion(+), 3 deletions(-) diff --git a/src/library/match.cpp b/src/library/match.cpp index 82fe3b34ab..85567159dc 100644 --- a/src/library/match.cpp +++ b/src/library/match.cpp @@ -178,8 +178,6 @@ class match_fn : public match_context { p = binding_body(p); t = binding_body(t); } - if (p.kind() == k || t.kind() == k) - return false; p = instantiate_rev(p, ls.size(), ls.data()); t = instantiate_rev(t, ls.size(), ls.data()); return _match(p, t); diff --git a/tests/lua/hop1.lua b/tests/lua/hop1.lua index 398e93d15c..31c0042bdc 100644 --- a/tests/lua/hop1.lua +++ b/tests/lua/hop1.lua @@ -25,4 +25,4 @@ assert(not match(F0(x), f(x, y))) local F0 = mk_idx_meta(0, Pi(x, N)) tst_match(Pi(x, y, F0(x)), Pi(x, y, f(f(x)))) tst_match(Fun(x, y, F0(x)), Fun(x, y, f(f(x)))) -assert(not match(Pi(x, F0(x)), Pi(x, y, f(f(x))))) +assert(match(Pi(x, F0(x)), Pi(x, y, f(f(x)))))