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

chore(library/rfl_lemmas): comment assertion

Browse source 
TODO: investigate why we have added it.
This commit is contained in:
Leonardo de Moura 2016-09-18 18:20:18 -07:00
parent 4e0e812811
commit 4ba9644bd7
1 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/library/rfl_lemmas.cpp
View file

@ -203,7 +203,8 @@ static bool instantiate_emetas(type_context & ctx, list<expr> const & _emetas, l
expr m = emetas[i];
unsigned mvar_idx = emetas.size() - 1 - i;
expr m_type = ctx.instantiate_mvars(ctx.infer(m));
lean_assert(!has_metavar(m_type));
// TODO(Leo, Daniel): do we need the following assertion?
// lean_assert(!has_expr_metavar(m_type));
if (ctx.get_tmp_mvar_assignment(mvar_idx)) continue;
if (instances[i]) {
if (auto v = ctx.mk_class_instance(m_type)) {