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

fix(frontends/lean/elaborator): visit_expr_quote bug

Browse source
This commit is contained in:
Leonardo de Moura 2018-05-29 16:21:52 -07:00
parent 0b1525b58e
commit 3615073faf
1 changed files with 2 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/frontends/lean/elaborator.cpp
View file

@ -3316,6 +3316,8 @@ expr elaborator::visit_expr_quote(expr const & e, optional<expr> const & expecte
});
s = Fun(locals, s);
expr new_s = visit(s, none_expr());
synthesize();
new_s = instantiate_mvars(new_s);
if (has_param_univ(new_s))
throw elaborator_exception(e, "invalid quotation, contains universe parameter");
if (has_univ_metavar(new_s))