fix(frontends/lean/pp): universe pretty printer

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

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));

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); }

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