From 323060df2631b68cc9ce07865b7aaee76312f3f2 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 18 May 2017 11:46:14 -0700
Subject: [PATCH] fix(frontends/lean/pp): pp for mutual definitions

missing line break
---
 src/frontends/lean/pp.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp
index 5f019f2793..7abf3b0e49 100644
--- a/src/frontends/lean/pp.cpp
+++ b/src/frontends/lean/pp.cpp
@@ -1084,7 +1084,7 @@ auto pretty_fn::pp_equations(expr const & e) -> optional<result> {
     unsigned eqnidx = 0;
     for (unsigned fidx = 0; fidx < num_fns; fidx++) {
         if (num_fns > 1) {
-            r += format("with") + space() + pp(fns[fidx]).fmt() + space() + colon() +
+            r += line() + format("with") + space() + pp(fns[fidx]).fmt() + space() + colon() +
                 space() + pp(mlocal_type(fns[fidx])).fmt();
         }
         if (eqnidx >= eqns.size()) return optional<result>();