From 55608c9b9f3a82e857a5d1b69ddbb51a1577b098 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 31 May 2015 11:01:21 -0700
Subject: [PATCH] fix(frontends/lean/pp): bug in pp arrow

---
 src/frontends/lean/pp.cpp           |  2 +-
 tests/lean/pp_bug.lean              | 11 +++++++++++
 tests/lean/pp_bug.lean.expected.out | 10 ++++++++++
 3 files changed, 22 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/pp_bug.lean
 create mode 100644 tests/lean/pp_bug.lean.expected.out

diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp
index 05c9ae5e9..1641e109c 100644
--- a/src/frontends/lean/pp.cpp
+++ b/src/frontends/lean/pp.cpp
@@ -709,7 +709,7 @@ auto pretty_fn::pp_pi(expr const & e) -> result {
         result lhs = pp_child(binding_domain(e), get_arrow_prec());
         result rhs = pp_child(lift_free_vars(binding_body(e), 1), get_arrow_prec()-1);
         format r   = group(lhs.fmt() + space() + (m_unicode ? *g_arrow_n_fmt : *g_arrow_fmt) + line() + rhs.fmt());
-        return result(get_arrow_prec()-1, r);
+        return result(get_arrow_prec(), get_arrow_prec()-1, r);
     } else {
         expr b = e;
         buffer<expr> locals;
diff --git a/tests/lean/pp_bug.lean b/tests/lean/pp_bug.lean
new file mode 100644
index 000000000..203568647
--- /dev/null
+++ b/tests/lean/pp_bug.lean
@@ -0,0 +1,11 @@
+variables p q : Prop
+check ¬(p → q)
+check ¬p → q
+check (¬p) → q
+check ¬(p → q)
+check p ↔ q
+check ¬(p ↔ q)
+check ¬p ↔ q
+check (¬p) ↔ q
+check (p → q) ↔ q
+check p → (q ↔ q)
diff --git a/tests/lean/pp_bug.lean.expected.out b/tests/lean/pp_bug.lean.expected.out
new file mode 100644
index 000000000..d927da623
--- /dev/null
+++ b/tests/lean/pp_bug.lean.expected.out
@@ -0,0 +1,10 @@
+¬(p → q) : Prop
+¬p → q : Prop
+¬p → q : Prop
+¬(p → q) : Prop
+p ↔ q : Prop
+¬(p ↔ q) : Prop
+¬p ↔ q : Prop
+¬p ↔ q : Prop
+p → q ↔ q : Prop
+p → (q ↔ q) : Prop