From b79794e60169c070ac1375964add4840c95230bc Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 29 Aug 2018 09:36:47 -0700
Subject: [PATCH] feat(frontends/lean/print_cmd): add basic support for testing
 new inductive datatype module

---
 src/frontends/lean/print_cmd.cpp | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/src/frontends/lean/print_cmd.cpp b/src/frontends/lean/print_cmd.cpp
index 4870141fa5..e4898bb9e1 100644
--- a/src/frontends/lean/print_cmd.cpp
+++ b/src/frontends/lean/print_cmd.cpp
@@ -376,6 +376,13 @@ void print_id_info(parser & p, message_builder & out, name const & id, bool show
             print_constant(p, out, "def", d, show_value);
             if (show_value)
                 print_definition(env, out, c, pos);
+        } else if (d.is_inductive()) {
+            print_constant(p, out, "(new) inductive", d);
+            out << "constructors:\n";
+            for (name const & n : d.to_inductive_val().get_cnstrs())
+                out << n << "\n";
+        } else if (d.is_constructor()) {
+            print_constant(p, out, "(new) constructor", d);
         }
         // print_patterns(p, c);
     }