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

chore(library/type_context): comment assertion violated by the pretty printer

Browse source
This commit is contained in:
Leonardo de Moura 2016-10-13 19:34:58 -07:00
parent 3162bac4e7
commit 0ee1eed751
1 changed files with 3 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/library/type_context.cpp
View file

@ -841,8 +841,9 @@ expr type_context::infer_metavar(expr const & e) {
if (!d) throw_unknown_metavar(e);
return d->get_type();
} else {
/* tmp metavariables should only occur in tmp_mode */
lean_assert(!is_idx_metavar(e) || in_tmp_mode());
/* tmp metavariables should only occur in tmp_mode.
The following assertion was commented because the pretty printer may violate it. */
// lean_assert(!is_idx_metavar(e) || in_tmp_mode());
return mlocal_type(e);
}
}