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

fix(library/user_recursors): invalid recursor_info for builtin indexed families

Browse source
This commit is contained in:
Leonardo de Moura 2015-05-19 12:19:46 -07:00
parent 6da2ba331f
commit 1e4285cf41
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

@ -61,8 +61,9 @@ recursor_info mk_recursor_info(environment const & env, name const & r, optional
motive_univ_pos = 0;
unsigned major_pos = *inductive::get_elim_major_idx(env, r);
unsigned num_indices = *inductive::get_num_indices(env, *I);
list<unsigned> params_pos = mk_list_range(0, *inductive::get_num_params(env, *I));
list<unsigned> indices_pos = mk_list_range(major_pos - num_indices, major_pos);
unsigned num_parms = *inductive::get_num_params(env, *I);
list<unsigned> params_pos = mk_list_range(0, num_parms);
list<unsigned> indices_pos = mk_list_range(num_parms, num_parms + num_indices);
return recursor_info(r, *I, motive_univ_pos, inductive::has_dep_elim(env, *I),
major_pos, params_pos, indices_pos);
}