From 62082c72a849bfa27a6e1fe69b176858cc9a310a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 18 May 2015 09:58:02 -0700 Subject: [PATCH] fix(library/user_recursors): remove unnecessary restriction on minor premises of user-defined recursors see issue #492 --- src/library/user_recursors.cpp | 10 ---------- tests/lean/hott/ind_tac2.hlean | 13 +++++++++++++ 2 files changed, 13 insertions(+), 10 deletions(-) create mode 100644 tests/lean/hott/ind_tac2.hlean diff --git a/src/library/user_recursors.cpp b/src/library/user_recursors.cpp index 979b11fa8..44586b690 100644 --- a/src/library/user_recursors.cpp +++ b/src/library/user_recursors.cpp @@ -165,16 +165,6 @@ recursor_info mk_recursor_info(environment const & env, name const & r) { if (!tc.is_def_eq(I_args_major[num_params + i], tele[first_index_pos + i]).first) throw_invalid_major(tele, I, num_params, num_indices, major_pos); } - for (unsigned i = 0; i < tele.size(); i++) { - if (info.is_minor(i)) { - buffer minor_tele; - expr minor_rtype = to_telescope(tc, mlocal_type(tele[i]), minor_tele); - expr minor_C = get_app_fn(minor_rtype); - if (!is_local(minor_C) || mlocal_name(minor_C) != mlocal_name(C)) - throw exception(sstream() << "invalid user defined recursor, resultant type of minor premise '" - << tele[i] << "' must be of the form (" << C << " ...)"); - } - } return info; } diff --git a/tests/lean/hott/ind_tac2.hlean b/tests/lean/hott/ind_tac2.hlean new file mode 100644 index 000000000..40c6f68b0 --- /dev/null +++ b/tests/lean/hott/ind_tac2.hlean @@ -0,0 +1,13 @@ +set_option pp.universes true + +check @trunc.rec_on + +attribute trunc.rec_on [recursor] + +print [recursor] trunc.rec_on + +check @type_quotient.rec_on + +attribute type_quotient.rec_on [recursor] + +print [recursor] type_quotient.rec_on