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

fix(frontends/lean/pp): bug in notation matching procedure

Browse source
This commit is contained in:
Leonardo de Moura 2014-10-19 10:48:41 -07:00
parent d7cc7cbd8c
commit 100b3abf1d
1 changed files with 1 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/frontends/lean/pp.cpp
View file

@ -609,9 +609,7 @@ bool pretty_fn::match(expr const & p, expr const & e, buffer<optional<expr>> & a
return true; return true;
} else if (is_placeholder(p)) { } else if (is_placeholder(p)) {
return true; return true;
} else if (is_constant(p)) { } else if (is_constant(p) && is_constant(e)) {
if (!is_constant(e))
return false;
levels p_ls = const_levels(p); levels p_ls = const_levels(p);
levels e_ls = const_levels(p); levels e_ls = const_levels(p);
while (!is_nil(p_ls)) { while (!is_nil(p_ls)) {