From ccfcd8279f82753e952bf2c9ce6e617c6cb7efcc Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 3 Sep 2018 16:41:51 -0700 Subject: [PATCH] fix(kernel/inductive): bug --- src/kernel/inductive.cpp | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/kernel/inductive.cpp b/src/kernel/inductive.cpp index 223bca5f22..db49143958 100644 --- a/src/kernel/inductive.cpp +++ b/src/kernel/inductive.cpp @@ -746,11 +746,10 @@ struct elim_nested_inductive_result { expr new_nested = instantiate_rev(abstract(nested, m_params.size(), m_params.data()), As.size(), As.data()); buffer I_args; expr I = get_app_args(new_nested, I_args); - lean_assert(I_args.size() == m_params.size()); lean_assert(is_constant(I)); name new_fn_name = const_name(fn).replace_prefix(auxI_name, const_name(I)); expr new_fn = mk_constant(new_fn_name, const_levels(I)); - expr new_t = mk_app(mk_app(new_fn, I_args), args.size() - I_args.size(), args.data() + I_args.size()); + expr new_t = mk_app(mk_app(new_fn, I_args), args.size() - m_params.size(), args.data() + m_params.size()); return some_expr(new_t); } }