From aff766430d8f2822abd05a0f29cbf1895d3d41aa Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 9 Jul 2014 19:17:00 -0700
Subject: [PATCH] fix(frontends/lean/pp): universe pretty printer

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/frontends/lean/pp.cpp         |  9 +++++++--
 src/frontends/lean/pp_options.cpp |  2 +-
 tests/lean/run/coe1.lean          | 30 ++++++++++++++++++++++++++++++
 3 files changed, 38 insertions(+), 3 deletions(-)
 create mode 100644 tests/lean/run/coe1.lean

diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp
index 8d158a053..813bad381 100644
--- a/src/frontends/lean/pp.cpp
+++ b/src/frontends/lean/pp.cpp
@@ -164,13 +164,18 @@ auto pretty_fn::pp_const(expr const & e) -> result {
             }
         }
     }
-    if (m_universes) {
+    if (m_universes && !empty(const_levels(e))) {
         format r = compose(format(n), format(".{"));
+        bool first = true;
         for (auto const & l : const_levels(e)) {
             format l_fmt = pp_level(l);
             if (is_max(l) || is_imax(l))
                 l_fmt = paren(l_fmt);
-            r += nest(m_indent, compose(line(), l_fmt));
+            if (first)
+                r += nest(m_indent, l_fmt);
+            else
+                r += nest(m_indent, compose(line(), l_fmt));
+            first = false;
         }
         r += format("}");
         return mk_result(group(r));
diff --git a/src/frontends/lean/pp_options.cpp b/src/frontends/lean/pp_options.cpp
index 9a68822f1..4b53335eb 100644
--- a/src/frontends/lean/pp_options.cpp
+++ b/src/frontends/lean/pp_options.cpp
@@ -48,7 +48,7 @@ RegisterBoolOption(g_pp_implicit,  LEAN_DEFAULT_PP_IMPLICIT,
                    "(lean pretty printer) display implicit parameters");
 RegisterBoolOption(g_pp_coercion,  LEAN_DEFAULT_PP_COERCION,
                    "(lean pretty printer) display coercions");
-RegisterBoolOption(g_pp_coercion,  LEAN_DEFAULT_PP_UNIVERSES,
+RegisterBoolOption(g_pp_universes,  LEAN_DEFAULT_PP_UNIVERSES,
                    "(lean pretty printer) display universes");
 
 unsigned get_pp_max_depth(options const & opts)  { return opts.get_unsigned(g_pp_max_depth, LEAN_DEFAULT_PP_MAX_DEPTH); }
diff --git a/tests/lean/run/coe1.lean b/tests/lean/run/coe1.lean
new file mode 100644
index 000000000..948b9d23c
--- /dev/null
+++ b/tests/lean/run/coe1.lean
@@ -0,0 +1,30 @@
+variable A : Type.{1}
+variable B : Type.{1}
+variable f : A → B
+coercion f
+variable g : B → B → B
+variables a1 a2 a3 : A
+variables b1 b2 b3 : B
+check g a1 b1
+set_option pp.coercion true
+check g a1 b1
+
+variable eq {A : Type} : A → A → Type.{0}
+check eq a1 a2
+check eq a1 b1
+set_option pp.implicit true
+check eq a1 b1
+set_option pp.universes true
+check eq a1 b1
+
+inductive pair (A : Type) (B: Type) : Type :=
+| mk_pair : A → B → pair A B
+
+check mk_pair a1 b2
+check B
+check mk_pair
+set_option pp.unicode false
+check mk_pair
+set_option pp.implicit false
+check mk_pair
+check pair
\ No newline at end of file