From b64e44fc44a2c98f410c707f8226475e07a103ce Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 5 Aug 2020 12:56:04 -0700 Subject: [PATCH] fix: allow kernel projections to be used in inductive families containing only one constructor --- src/kernel/type_checker.cpp | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp index c95033c38a..c3c9c278f6 100644 --- a/src/kernel/type_checker.cpp +++ b/src/kernel/type_checker.cpp @@ -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);