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

fix(library/match): bug in higher-order matcher

Browse source
This commit is contained in:
Leonardo de Moura 2015-05-14 18:21:17 -07:00
parent 7f8afcf04b
commit 1dedd2829c
2 changed files with 1 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/library/match.cpp
View file

@ -178,8 +178,6 @@ class match_fn : public match_context {
p = binding_body(p); p = binding_body(p);
t = binding_body(t); t = binding_body(t);
} }
if (p.kind() == k || t.kind() == k)
return false;
p = instantiate_rev(p, ls.size(), ls.data()); p = instantiate_rev(p, ls.size(), ls.data());
t = instantiate_rev(t, ls.size(), ls.data()); t = instantiate_rev(t, ls.size(), ls.data());
return _match(p, t); return _match(p, t);

2
tests/lua/hop1.lua
View file

@ -25,4 +25,4 @@ assert(not match(F0(x), f(x, y)))
local F0 = mk_idx_meta(0, Pi(x, N)) local F0 = mk_idx_meta(0, Pi(x, N))
tst_match(Pi(x, y, F0(x)), Pi(x, y, f(f(x)))) 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)))) 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)))))