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

fix: allow kernel projections to be used in inductive families containing only one constructor

Browse source
This commit is contained in:
Leonardo de Moura 2020-08-05 12:56:04 -07:00
parent 5aceea2632
commit b64e44fc44
1 changed files with 4 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/kernel/type_checker.cpp
View file

@ -242,15 +242,16 @@ expr type_checker::infer_proj(expr const & e, bool infer_only) {
if (!I_info.is_inductive())
throw invalid_proj_exception(env(), m_lctx, e);
inductive_val I_val = I_info.to_inductive_val();
if (length(I_val.get_cnstrs()) != 1 || args.size() != I_val.get_nparams())
if (length(I_val.get_cnstrs()) != 1 || args.size() != I_val.get_nparams() + I_val.get_nindices())
throw invalid_proj_exception(env(), m_lctx, e);
constant_info c_info = env().get(head(I_val.get_cnstrs()));
expr r = instantiate_type_lparams(c_info, const_levels(I));
for (expr const & arg : args) {
for (unsigned i = 0; i < I_val.get_nparams(); i++) {
lean_assert(i < args.size());
r = whnf(r);
if (!is_pi(r)) throw invalid_proj_exception(env(), m_lctx, e);
r = instantiate(binding_body(r), arg);
r = instantiate(binding_body(r), args[i]);
}
for (unsigned i = 0; i < idx; i++) {
r = whnf(r);