fix(frontends/lean/pp): bug in pretty printer notation match procedure

This commit is contained in:
Leonardo de Moura 2014-10-20 18:58:27 -07:00
parent 2e9141b7e1
commit 8a44dfc1df
3 changed files with 16 additions and 0 deletions

View file

@ -612,6 +612,8 @@ bool pretty_fn::match(expr const & p, expr const & e, buffer<optional<expr>> & a
} else if (is_placeholder(p)) { } else if (is_placeholder(p)) {
return true; return true;
} else if (is_constant(p) && is_constant(e)) { } else if (is_constant(p) && is_constant(e)) {
if (const_name(p) != const_name(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)) {

View file

@ -0,0 +1,9 @@
import logic data.num
open num
notation `o` := 10
check 11
constant f : num → num
check o + 1
check f o + o + o
eval 9 + 1
eval o+4

View file

@ -0,0 +1,5 @@
11 : num
o + 1 : num
f o + o + o : num
o
14