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

fix(library/user_recursors): warning message

Browse source
This commit is contained in:
Leonardo de Moura 2015-05-13 09:42:32 -07:00
parent 065a1f7501
commit dd5b221d32
1 changed files with 3 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/library/user_recursors.cpp
View file

@ -106,12 +106,13 @@ recursor_info mk_recursor_info(environment const & env, name const & r) {
"motive result sort must be Type.{l} where l is a universe parameter");
}
name l = param_id(C_lvl);
C_univ_pos = 0;
unsigned uni_pos = 0;
for (name const & l_curr : d.get_univ_params()) {
if (l_curr == l)
break;
C_univ_pos = *C_univ_pos + 1;
uni_pos++;
}
C_univ_pos = uni_pos;
lean_assert(*C_univ_pos < length(d.get_univ_params()));
}