From 6493ff53884e6c9f8ddb8caa6d6182aec106e84b Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 9 May 2014 19:50:04 -0700
Subject: [PATCH] fix(kernel/formatter): print level parameters

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/kernel/formatter.cpp | 16 +++++++++++++++-
 1 file changed, 15 insertions(+), 1 deletion(-)

diff --git a/src/kernel/formatter.cpp b/src/kernel/formatter.cpp
index 11bd1e2fa..bc2fcd334 100644
--- a/src/kernel/formatter.cpp
+++ b/src/kernel/formatter.cpp
@@ -70,6 +70,20 @@ struct print_expr_fn {
         print_child(binder_body(e), extend(c, binder_name(e), binder_domain(e)));
     }
 
+    void print_const(expr const & a) {
+        list<level> const & ls = const_level_params(a);
+        out() << const_name(a);
+        if (!is_nil(ls)) {
+            out() << ".{";
+            bool first = true;
+            for (auto l : ls) {
+                if (first) first = false; else out() << " ";
+                out() << l;
+            }
+            out() << "}";
+        }
+    }
+
     void print(expr const & a, context const & c) {
         switch (a.kind()) {
         case expr_kind::Meta: case expr_kind::Local:
@@ -84,7 +98,7 @@ struct print_expr_fn {
             break;
         }
         case expr_kind::Constant:
-            out() << const_name(a);
+            print_const(a);
             break;
         case expr_kind::App:
             print_app(a, c);