michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(frontends/lean): add 'print definition' command

Browse source
This commit is contained in:
Leonardo de Moura 2014-10-23 14:52:24 -07:00
parent 04b4e36701
commit a6571c3273
1 changed files with 9 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/frontends/lean/builtin_cmds.cpp
View file

@ -66,6 +66,15 @@ environment print_cmd(parser & p) {
} else if (p.curr_is_token_or_id(get_options_tk())) {
p.next();
p.regular_stream() << p.ios().get_options() << endl;
} else if (p.curr_is_token_or_id(get_definition_tk())) {
p.next();
auto pos = p.pos();
name c = p.check_constant_next("invalid 'print definition', constant expected");
environment const & env = p.env();
declaration d = env.get(c);
if (!d.is_definition())
throw parser_error(sstream() << "invalid 'print definition', '" << c << "' is not a definition", pos);
p.regular_stream() << d.get_value() << endl;
} else if (p.curr_is_token_or_id(get_instances_tk())) {
p.next();
name c = p.check_constant_next("invalid 'print instances', constant expected");