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

feat(kernel/inductive): v_idx ==> ih_idx

Browse source
This commit is contained in:
Leonardo de Moura 2016-10-05 17:13:52 -07:00
parent 68df31df67
commit 1b628930ba
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/kernel/inductive/inductive.cpp
View file

@ -610,7 +610,7 @@ struct add_inductive_fn {
C_app = mk_app(C_app, u_app);
}
expr v_i_ty = Pi(xs, C_app);
expr v_i = mk_local(mk_fresh_name(), name("v").append_after(i), v_i_ty, binder_info());
expr v_i = mk_local(mk_fresh_name(), name("ih").append_after(i+1), v_i_ty, binder_info());
v.push_back(v_i);
}
expr minor_ty = Pi(b, Pi(u, Pi(v, C_app)));