From 88d55bfef0b55552407c43b98bd4cd25b194efd7 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 29 Oct 2014 13:42:50 -0700 Subject: [PATCH] fix(library/definitional/projection): remove redundant 'error in' --- src/library/definitional/projection.cpp | 12 ++++++------ tests/lean/proj.lean.expected.out | 14 +++++++------- 2 files changed, 13 insertions(+), 13 deletions(-) diff --git a/src/library/definitional/projection.cpp b/src/library/definitional/projection.cpp index df5de6d64..634700809 100644 --- a/src/library/definitional/projection.cpp +++ b/src/library/definitional/projection.cpp @@ -14,23 +14,23 @@ Author: Leonardo de Moura namespace lean { [[ noreturn ]] static void throw_ill_formed(name const & n) { - throw exception(sstream() << "error in projection generation, '" << n << "' is an ill-formed inductive datatype"); + throw exception(sstream() << "projection generation, '" << n << "' is an ill-formed inductive datatype"); } static pair get_nparam_intro_rule(environment const & env, name const & n) { optional decls = inductive::is_inductive_decl(env, n); if (!decls) - throw exception(sstream() << "error in projection generation, '" << n << "' is not an inductive datatype"); + throw exception(sstream() << "projection generation, '" << n << "' is not an inductive datatype"); optional num_indices = inductive::get_num_indices(env, n); if (num_indices && *num_indices > 0) - throw exception(sstream() << "error in projection generation, '" + throw exception(sstream() << "projection generation, '" << n << "' is an indexed inductive datatype family"); unsigned num_params = std::get<1>(*decls); for (auto const & decl : std::get<2>(*decls)) { if (inductive::inductive_decl_name(decl) == n) { auto intros = inductive::inductive_decl_intros(decl); if (length(intros) != 1) - throw exception(sstream() << "error in projection generation, '" + throw exception(sstream() << "projection generation, '" << n << "' does not have a single constructor"); return mk_pair(num_params, head(intros)); } @@ -60,7 +60,7 @@ environment mk_projections(environment const & env, name const & n, buffer name rec_name = inductive::get_elim_name(n); declaration ind_decl = env.get(n); if (env.impredicative() && is_prop(ind_decl.get_type())) - throw exception(sstream() << "error in projection generation, '" << n << "' is a proposition"); + throw exception(sstream() << "projection generation, '" << n << "' is a proposition"); declaration rec_decl = env.get(rec_name); level_param_names lvl_params = ind_decl.get_univ_params(); levels lvls = param_names_to_levels(lvl_params); @@ -86,7 +86,7 @@ environment mk_projections(environment const & env, name const & n, buffer environment new_env = env; for (name const & proj_name : proj_names) { if (!is_pi(intro_type)) - throw exception(sstream() << "error generating projection '" << proj_name << "', '" + throw exception(sstream() << "generating projection '" << proj_name << "', '" << n << "' does not have sufficient data"); expr result_type = binding_domain(intro_type); buffer proj_args; diff --git a/tests/lean/proj.lean.expected.out b/tests/lean/proj.lean.expected.out index a0c06dfa7..c0f4521e6 100644 --- a/tests/lean/proj.lean.expected.out +++ b/tests/lean/proj.lean.expected.out @@ -1,8 +1,8 @@ -proj.lean:7:0: error: error in projection generation, 'or' does not have a single constructor -proj.lean:8:0: error: error in projection generation, 'and' is a proposition -proj.lean:9:0: error: error in projection generation, 'eq.refl' is not an inductive datatype -proj.lean:10:0: error: error in projection generation, 'eq' is an indexed inductive datatype family -proj.lean:11:0: error: error in projection generation, 'vector' is an indexed inductive datatype family -proj.lean:16:0: error: error generating projection 'point.z', 'point' does not have sufficient data +proj.lean:7:0: error: projection generation, 'or' does not have a single constructor +proj.lean:8:0: error: projection generation, 'and' is a proposition +proj.lean:9:0: error: projection generation, 'eq.refl' is not an inductive datatype +proj.lean:10:0: error: projection generation, 'eq' is an indexed inductive datatype family +proj.lean:11:0: error: projection generation, 'vector' is an indexed inductive datatype family +proj.lean:16:0: error: generating projection 'point.z', 'point' does not have sufficient data proj.lean:20:0: error: invalid object declaration, environment already has an object named 'point.x' -proj.lean:25:0: error: error in projection generation, 'funny' is an indexed inductive datatype family +proj.lean:25:0: error: projection generation, 'funny' is an indexed inductive datatype family