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

fix(library/lazy_abstraction): incorrect assertion

Browse source
This commit is contained in:
Leonardo de Moura 2016-06-11 20:28:54 -07:00
parent 125a80ad69
commit bc47eca2ff
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/library/lazy_abstraction.cpp
View file

@ -102,7 +102,7 @@ struct push_lazy_abstraction_fn : public replace_visitor {
void add_vidxs(int v) {
for (pair<name, unsigned> & p : m_s) {
lean_assert(static_cast<int>(p.second) + v > 0);
lean_assert(static_cast<int>(p.second) + v >= 0);
p.second += v;
}
m_cache.clear();