diff --git a/src/frontends/lean/print_cmd.cpp b/src/frontends/lean/print_cmd.cpp index b9bcafd087..dc809282f3 100644 --- a/src/frontends/lean/print_cmd.cpp +++ b/src/frontends/lean/print_cmd.cpp @@ -392,7 +392,7 @@ void print_id_info(parser & p, message_builder & out, name const & id, bool show print_constant(p, out, "(new) recursor", d); out << "reduction rules\n"; for (recursor_rule const & rule : d.to_recursor_val().get_rules()) { - out << rule.get_constructor() << " ==>\n" << rule.get_rhs() << "\n"; + out << rule.get_cnstr() << " ==>\n" << rule.get_rhs() << "\n"; } } // print_patterns(p, c); diff --git a/src/kernel/declaration.h b/src/kernel/declaration.h index 00c7a2241e..66e11e3428 100644 --- a/src/kernel/declaration.h +++ b/src/kernel/declaration.h @@ -312,7 +312,7 @@ public: recursor_rule(recursor_rule && other):object_ref(other) {} recursor_rule & operator=(recursor_rule const & other) { object_ref::operator=(other); return *this; } recursor_rule & operator=(recursor_rule && other) { object_ref::operator=(other); return *this; } - name const & get_constructor() const { return static_cast(cnstr_obj_ref(*this, 0)); } + name const & get_cnstr() const { return static_cast(cnstr_obj_ref(*this, 0)); } unsigned get_nfields() const { return static_cast(cnstr_obj_ref(*this, 1)).get_small_value(); } expr const & get_rhs() const { return static_cast(cnstr_obj_ref(*this, 2)); } }; diff --git a/src/kernel/inductive.cpp b/src/kernel/inductive.cpp index d5be4763b8..890b9cf45f 100644 --- a/src/kernel/inductive.cpp +++ b/src/kernel/inductive.cpp @@ -992,7 +992,7 @@ environment environment::add_inductive(declaration const & d) const { buffer new_rules; for (recursor_rule const & rule : rec_val.get_rules()) { expr new_rhs = res.restore_nested(rule.get_rhs(), aux_env, aux_rec_name_map); - name cnstr_name = rule.get_constructor(); + name cnstr_name = rule.get_cnstr(); name new_cnstr_name = cnstr_name; if (new_rec_name != rec_name) { /* We need to fix the constructor name */