From b2f8d2000c95fddd6ed7d8c5b3d31608070bc954 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 1 Jun 2015 22:23:34 -0700 Subject: [PATCH] fix(library/simplifier/rewrite_rule_set): avoid compiler specific behavior --- src/library/simplifier/rewrite_rule_set.cpp | 4 +++- tests/lean/rw_set3.lean.expected.out | 2 +- 2 files changed, 4 insertions(+), 2 deletions(-) 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