diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index dbd19acb23..abb14aa90c 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/src/frontends/lean/builtin_cmds.cpp @@ -447,6 +447,12 @@ environment print_cmd(parser & p) { for (name const & i : get_class_instances(env, c)) { p.regular_stream() << i << " : " << env.get(i).get_type() << endl; } + if (list derived_insts = get_class_derived_trans_instances(env, c)) { + p.regular_stream() << "Derived transitive instances:\n"; + for (name const & i : derived_insts) { + p.regular_stream() << i << " : " << env.get(i).get_type() << endl; + } + } } else if (p.curr_is_token_or_id(get_classes_tk())) { p.next(); environment const & env = p.env();