diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp index f6c9a03a9..f60f99aaf 100644 --- a/src/frontends/lean/pp.cpp +++ b/src/frontends/lean/pp.cpp @@ -609,9 +609,7 @@ bool pretty_fn::match(expr const & p, expr const & e, buffer> & a return true; } else if (is_placeholder(p)) { return true; - } else if (is_constant(p)) { - if (!is_constant(e)) - return false; + } else if (is_constant(p) && is_constant(e)) { levels p_ls = const_levels(p); levels e_ls = const_levels(p); while (!is_nil(p_ls)) {