diff --git a/src/library/simplifier/rewrite_rule_set.cpp b/src/library/simplifier/rewrite_rule_set.cpp index d0f561585..b29ed8ac2 100644 --- a/src/library/simplifier/rewrite_rule_set.cpp +++ b/src/library/simplifier/rewrite_rule_set.cpp @@ -28,7 +28,9 @@ format rewrite_rule::pp(formatter const & fmt) const { r += format("#") + format(length(m_metas)); if (m_is_permutation) r += space() + format("perm"); - r += group(comma() + space() + fmt(m_lhs) + space() + format("↦") + pp_indent_expr(fmt, m_rhs)); + format r1 = comma() + space() + fmt(m_lhs); + r1 += space() + format("↦") + pp_indent_expr(fmt, m_rhs); + r += group(r1); return r; } diff --git a/tests/lean/rw_set3.lean.expected.out b/tests/lean/rw_set3.lean.expected.out index bcf43ff6e..a5353e9c2 100644 --- a/tests/lean/rw_set3.lean.expected.out +++ b/tests/lean/rw_set3.lean.expected.out @@ -1,2 +1,2 @@ rewrite rules for eq -#2 perm, nat.add ?M_2 ?M_1 ↦ nat.add ?M_1 ?M_2 +#2 perm, nat.add ?M_1 ?M_2 ↦ nat.add ?M_2 ?M_1