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