From fbf2d5d300298dca6582099f064fd49ce2e656d4 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 15 Jul 2020 10:00:39 -0700
Subject: [PATCH] fix: do not print as arrow if binder_info is not the default
 one

---
 src/library/print.cpp | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/src/library/print.cpp b/src/library/print.cpp
index e7df3735ce..48282f6693 100644
--- a/src/library/print.cpp
+++ b/src/library/print.cpp
@@ -147,6 +147,10 @@ struct print_expr_fn {
         print_child(app_arg(e));
     }
 
+    static bool is_arrow(expr const & t) {
+        return lean::is_arrow(t) && binding_info(t) == binder_info::Default;
+    }
+
     void print_arrow_body(expr const & a) {
         if (is_atomic(a) || is_arrow(a))
             return print(a);