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

fix(library/tactic/simplifier/simplifier): assertion

Browse source
This commit is contained in:
Leonardo de Moura 2016-09-19 11:29:03 -07:00
parent 10f4a22fff
commit 0a6f571f07
1 changed files with 7 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/library/tactic/simplifier/simplifier.cpp
View file

@ -1084,7 +1084,13 @@ simp_result simplifier::try_congr(expr const & e, user_congr_lemma const & cl) {
flet<simp_lemmas> set_ctx_slss(m_ctx_slss, m_contextual ? add_to_slss(m_ctx_slss, local_factory.as_buffer()) : m_ctx_slss);
h_lhs = tmp_tctx.instantiate_mvars(h_lhs);
lean_assert(!has_metavar(h_lhs));
/* TODO(Leo, Daniel): the original assertion was !has_metavar(h_lhs).
It is incorrect. I got an assertion violation when processing
a term containing universe meta-variables. So, I relaxed it to !has_expr_metavar(h_lhs).
We should investigate this. Example: what happens if the input expression has
regular meta-variables? Perhaps, the right assertion is: h_lhs does *not* have temporary
universe and regular meta-variables. */
lean_assert(!has_expr_metavar(h_lhs));
if (m_contextual) {
freset<simplify_cache> reset_cache(m_cache);