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

feat(frontends/lean/builtin_cmds): improve error message

Browse source
This commit is contained in:
Leonardo de Moura 2016-05-13 16:26:34 -07:00
parent 7242de7238
commit c2959dc77b
1 changed files with 0 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -665,11 +665,8 @@ static environment compile_cmd(parser & p) {
}
static environment vm_eval_cmd(parser & p) {
auto pos = p.pos();
expr e; level_param_names ls;
std::tie(e, ls) = parse_local_expr(p);
if (has_local(e) || has_metavar(e))
throw parser_error("invalid vm_eval command, argument must be a closed expression", pos);
type_checker tc(p.env());
expr type = tc.infer(e);
environment new_env = p.env();