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

fix(library/user_recursors): missing statement

Browse source
This commit is contained in:
Leonardo de Moura 2016-08-22 09:38:43 -07:00
parent ccf9187704
commit 2587164999
1 changed files with 1 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/library/user_recursors.cpp
View file

@ -110,6 +110,7 @@ recursor_info mk_recursor_info(environment const & env, name const & r, optional
name I = r.get_prefix();
unsigned num_indices = *inductive::get_num_indices(env, I);
unsigned num_params = *inductive::get_num_params(env, I);
has_given_major_pos = true;
given_major_pos = num_params + 1 /* motive */ + num_indices;
}
declaration d = env.get(r);