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

feat(library/type_context): do not cache whnf in tmp_mode if term contains metavariables

Browse source
This commit is contained in:
Leonardo de Moura 2017-04-13 18:15:34 -07:00
parent 7cc68130b3
commit fe0b694a06
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/type_context.cpp
View file

@ -831,7 +831,8 @@ expr type_context::whnf(expr const & e) {
if (auto next_t = unfold_definition(t1)) {
t = *next_t;
} else {
if (!m_used_assignment && !is_stuck(t1) &&
if ((!in_tmp_mode() || !has_expr_metavar(t1)) &&
!m_used_assignment && !is_stuck(t1) &&
postponed_sz == m_postponed.size() && !m_transparency_pred && !m_unfold_pred) {
cache.insert(mk_pair(e, t1));
}