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

fix(frontends/lean/builtin_cmds): abort eval after error recovery and complain about unsynthesized mvars early

Browse source
This commit is contained in:
Sebastian Ullrich 2017-05-31 16:05:47 +02:00
parent 9fa31b2858
commit f820f3f97e
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -432,9 +432,9 @@ static environment compile_cmd(parser & p) {
static environment eval_cmd(parser & p) {
auto pos = p.pos();
expr e; level_param_names ls;
std::tie(e, ls) = parse_local_expr(p, "_eval");
if (has_metavar(e))
throw parser_error("invalid eval command, expression contains metavariables", pos);
std::tie(e, ls) = parse_local_expr(p, "_eval", /* relaxed */ false);
if (has_synthetic_sorry(e))
return p.env();
type_context tc(p.env(), transparency_mode::All);
auto type = tc.infer(e);