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

fix(library/type_context): assertion violation at unification hints

Browse source
This commit is contained in:
Leonardo de Moura 2016-12-05 20:51:03 -08:00
parent ef6d6075bb
commit 72ce00d3d0
1 changed files with 1 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/library/type_context.cpp
View file

@ -2593,10 +2593,8 @@ public:
auto instantiate_assignment_fn = [&](expr const & e, unsigned offset) {
if (is_var(e)) {
unsigned idx = var_idx(e) + offset;
if (idx < m_assignment.size()) {
lean_assert(m_assignment[idx]);
if (idx < m_assignment.size() && m_assignment[idx])
return m_assignment[idx];
}
}
return none_expr();
};