Display context_entry body when pretty printing contexts.

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

src/kernel/context.cpp

@@ -41,11 +41,19 @@ format pp(expr_formatter & fmt, context const & c) {
         if (tail(c))
             r = format{pp(fmt, tail(c)), line()};
         context_entry const & e = head(c);
-        if (e.get_name().is_anonymous())
+        format new_entry;
-            r += format("_");
+        unsigned name_sz;
-        else
+        if (e.get_name().is_anonymous()) {
-            r += format(e.get_name());
+            new_entry = format("_");
-        r += format{space(), colon(), space(), fmt(e.get_domain(), tail(c))};
+            name_sz = 1;
+        } else {
+            new_entry = format(e.get_name());
+            name_sz = e.get_name().size();
+        }
+        new_entry += format{space(), colon(), space(), nest(name_sz + 3, fmt(e.get_domain(), tail(c)))};
+        if (e.get_body())
+            new_entry += format{space(), format(":="), fmt.nest(format{line(), fmt(e.get_body(), tail(c))})};
+        r += group(new_entry);
         return r;
     } else {
         return format();

src/tests/kernel/type_check.cpp

@@ -148,6 +148,25 @@ static void tst8() {
     }
 }
 
+static void tst9() {
+    environment env = mk_toplevel();
+    env.add_var("P", arrow(Int, arrow(Int, Bool)));
+    env.add_var("x", Int);
+    expr P = Const("P");
+    context c;
+    c = extend(c, "P", arrow(Bool, Bool));
+    c = extend(c, "P", Bool, Var(0)(True));
+    c = extend(c, "H", Var(1)(True));
+    c = extend(c, "x", Bool);
+    expr t = P(Const("x"), Var(0));
+    try {
+        infer_type(t, env, c);
+        lean_unreachable();
+    } catch (exception & ex) {
+        std::cout << "Error: " << ex.what() << "\n";
+    }
+}
+
 int main() {
     tst1();
     tst2();
@@ -157,5 +176,6 @@ int main() {
     tst6();
     tst7();
     tst8();
+    tst9();
     return has_violations() ? 1 : 0;
 }