From 3ba777e70977f4bb8d275ce8a21f5dd6bffefe97 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 11 Sep 2018 17:54:24 -0700
Subject: [PATCH] fix(frontends/lean/pp): do not pp `let` type when
 `m_binder_types == false`

---
 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 26644b95b4..3d1430d01c 100644
--- a/src/frontends/lean/pp.cpp
+++ b/src/frontends/lean/pp.cpp
@@ -1165,7 +1165,7 @@ auto pretty_fn::pp_let(expr e) -> result {
         format sep     = i < sz - 1 ? comma() : format();
         format entry   = format(n);
         format v_fmt   = pp_child(v, 0).fmt();
-        if (is_neutral_expr(t)) {
+        if (!m_binder_types || is_neutral_expr(t)) {
             entry += space() + *g_assign_fmt + nest(m_indent, line() + v_fmt + sep);
         } else {
             format t_fmt   = pp_child(t, 0).fmt();