michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(library/user_recursors): bug at get_num_minors

Browse source
This commit is contained in:
Leonardo de Moura 2015-11-15 11:48:34 -08:00
parent 676ffb77f9
commit e18e4e3200
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/library/user_recursors.cpp
View file

@ -24,8 +24,8 @@ bool recursor_info::is_minor(unsigned pos) const {
unsigned recursor_info::get_num_minors() const { unsigned recursor_info::get_num_minors() const {
unsigned r = m_num_args; unsigned r = m_num_args;
lean_assert(r >= get_motive_pos()); lean_assert(r >= get_motive_pos() + 1);
r -= get_motive_pos(); r -= (get_motive_pos() + 1);
lean_assert(m_major_pos >= get_first_index_pos()); lean_assert(m_major_pos >= get_first_index_pos());
lean_assert(r >= m_major_pos - get_first_index_pos() + 1); lean_assert(r >= m_major_pos - get_first_index_pos() + 1);
r -= (m_major_pos - get_first_index_pos() + 1); r -= (m_major_pos - get_first_index_pos() + 1);