max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(frontends/lean/print_cmd): add basic support for testing new inductive datatype module

Browse source
This commit is contained in:
Leonardo de Moura 2018-08-29 09:36:47 -07:00
parent 863355c6a0
commit b79794e601
1 changed files with 7 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/frontends/lean/print_cmd.cpp
View file

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