From fbb021386c7d3b361eef0598d0147af8f5cfd69d Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 20 Aug 2013 08:09:39 -0700
Subject: [PATCH] Add minor improvement to pretty printer

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 examples/ex10.lean  | 19 +++++++++++++++++++
 src/frontend/pp.cpp |  5 ++---
 2 files changed, 21 insertions(+), 3 deletions(-)
 create mode 100644 examples/ex10.lean

diff --git a/examples/ex10.lean b/examples/ex10.lean
new file mode 100644
index 000000000..d089e297e
--- /dev/null
+++ b/examples/ex10.lean
@@ -0,0 +1,19 @@
+(* Define a "fake" type to simulate the natural numbers. This is just a test. *)
+Variable Natural : Type
+Variable lt : Natural -> Natural -> Bool
+Variable zero : Natural
+Variable one : Natural
+Variable two : Natural
+Variable three : Natural
+Infix 50 < : lt
+Axiom two_lt_three : two < three
+Definition vector (A : Type) (n : Natural) : Type := Pi (i : Natural) (H : i < n), A
+Definition const (A : Type) (n : Natural) (d : A) : vector A n := fun (i : Natural) (H : i < n), d
+Definition update (A : Type) (n : Natural) (v : vector A n) (i : Natural) (d : A) : vector A n := fun (j : Natural) (H : j < n), if A (j = i) d (v j H)
+Definition select (A : Type) (n : Natural) (v : vector A n) (i : Natural) (H : i < n) : A := v i H
+Environment
+Check select Bool three (update Bool three (const Bool three false) two true) two two_lt_three
+Eval select Bool three (update Bool three (const Bool three false) two true) two two_lt_three
+Check select
+
+
diff --git a/src/frontend/pp.cpp b/src/frontend/pp.cpp
index a9dfb01d7..6e2059131 100644
--- a/src/frontend/pp.cpp
+++ b/src/frontend/pp.cpp
@@ -478,7 +478,7 @@ class pp_fn {
        condensed definitions. \see pp_abstraction_core.
     */
     std::pair<expr, expr> collect_nested(expr const & e, expr T, expr_kind k, buffer<std::pair<name, expr>> & r) {
-        if (e.kind() == k) {
+        if (e.kind() == k && (!T || is_abstraction(T))) {
             name n1    = get_unused_name(e);
             r.push_back(mk_pair(n1, abst_domain(e)));
             expr b = instantiate_with_closed(abst_body(e), mk_constant(n1));
@@ -567,7 +567,6 @@ class pp_fn {
             auto p = collect_nested(e, T, e.kind(), nested);
             expr b = p.first;
             T = p.second;
-            lean_assert(b.kind() != e.kind());
             format head;
             if (!T) {
                 head = is_lambda(e) ? g_lambda_fmt : g_Pi_fmt;
@@ -845,7 +844,7 @@ class pp_formatter_cell : public formatter_cell {
             it1 = abst_body(it1);
             it2 = abst_body(it2);
         }
-        if (!is_lambda(v) || is_pi(it1) || is_lambda(it2)) {
+        if (!is_lambda(v) || is_pi(it1)) {
             return pp_definition(kwd, n, t, v);
         } else {
             lean_assert(is_lambda(v));