diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index c4d9a130ad..15934f388d 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -106,7 +106,7 @@ elaborator_strategy get_elaborator_strategy(environment const & env, name const if (auto data = get_elaborator_strategy_attribute().get(env, n)) return data->m_status; - if (env.get(n).is_recursor() || + if (is_recursor(env, n) || is_aux_recursor(env, n) || is_user_defined_recursor(env, n)) { return elaborator_strategy::AsEliminator; @@ -395,7 +395,7 @@ static bool is_basic_aux_recursor(environment const & env, name const & n) { /** See comment at elim_info */ auto elaborator::get_elim_info_for_builtin(name const & fn) -> elim_info { - lean_assert(is_basic_aux_recursor(m_env, fn) || m_env.get(fn).is_recursor()); + lean_assert(is_basic_aux_recursor(m_env, fn) || is_recursor(m_env, fn)); /* Remark: this is not just an optimization. The code at use_elim_elab_core only works for dependent elimination. */ lean_assert(!fn.is_atomic()); @@ -440,7 +440,7 @@ auto elaborator::get_elim_info_for_builtin(name const & fn) -> elim_info { auto elaborator::use_elim_elab_core(name const & fn) -> optional { if (!is_elim_elab_candidate(fn)) return optional(); - if (is_basic_aux_recursor(m_env, fn) || m_env.get(fn).is_recursor()) { + if (is_basic_aux_recursor(m_env, fn) || is_recursor(m_env, fn)) { return optional(get_elim_info_for_builtin(fn)); } type_context_old::tmp_locals locals(m_ctx); diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 01f6e5e500..ab74fc18d2 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -1385,7 +1385,7 @@ struct to_pattern_fn { /* Return true iff the constant n may occur in a pattern */ bool is_pattern_constant(name const & n) { - if (env().get(n).is_constructor()) + if (is_constructor(env(), n)) return true; if (has_pattern_attribute(env(), n)) return true; diff --git a/src/library/equations_compiler/elim_match.cpp b/src/library/equations_compiler/elim_match.cpp index 9388a10199..59d4f0d3a6 100644 --- a/src/library/equations_compiler/elim_match.cpp +++ b/src/library/equations_compiler/elim_match.cpp @@ -275,7 +275,7 @@ struct elim_match_fn { return optional(); } - bool is_inductive(name const & n) const { return m_env.get(n).is_inductive(); } + bool is_inductive(name const & n) const { return ::lean::is_inductive(m_env, n); } bool is_inductive(expr const & e) const { return is_constant(e) && is_inductive(const_name(e)); } bool is_inductive_app(expr const & e) const { return is_inductive(get_app_fn(e)); } diff --git a/src/library/equations_compiler/structural_rec.cpp b/src/library/equations_compiler/structural_rec.cpp index b8c1da1505..aa2e33c5c6 100644 --- a/src/library/equations_compiler/structural_rec.cpp +++ b/src/library/equations_compiler/structural_rec.cpp @@ -75,7 +75,7 @@ struct structural_rec_fn { m_ctx(ctx), m_lhs(lhs), m_fn(fn), m_pattern(pattern), m_arg_idx(arg_idx) {} bool is_constructor(expr const & e) const { - return is_constant(e) && m_ctx.env().get(const_name(e)).is_constructor(); + return is_constant(e) && ::lean::is_constructor(m_ctx.env(), const_name(e)); } expr whnf(expr const & e) { @@ -220,7 +220,7 @@ struct structural_rec_fn { expr arg_type = ctx.relaxed_whnf(binding_domain(fn_type)); buffer I_args; expr I = get_app_args(arg_type, I_args); - if (!is_constant(I) || !m_env.get(const_name(I)).is_inductive()) { + if (!is_constant(I) || !is_inductive(m_env, const_name(I))) { trace_struct(tout() << "structural recursion on argument #" << (arg_idx+1) << " was not used " << "for '" << fn << "' because type is not inductive\n " << arg_type << "\n";); diff --git a/src/library/equations_compiler/util.cpp b/src/library/equations_compiler/util.cpp index c8fe3ad458..8f0f33a1b9 100644 --- a/src/library/equations_compiler/util.cpp +++ b/src/library/equations_compiler/util.cpp @@ -322,7 +322,7 @@ bool is_nat_int_char_string_name_value(type_context_old & ctx, expr const & e) { } static bool is_inductive(environment const & env, expr const & e) { - return is_constant(e) && env.get(const_name(e)).is_inductive(); + return is_constant(e) && is_inductive(env, const_name(e)); } /* Normalize until head is an inductive datatype */ diff --git a/src/library/tactic/cases_tactic.cpp b/src/library/tactic/cases_tactic.cpp index 5fdb913f6b..e881723ebc 100644 --- a/src/library/tactic/cases_tactic.cpp +++ b/src/library/tactic/cases_tactic.cpp @@ -102,7 +102,7 @@ struct cases_tactic_fn { expr const & fn = get_app_args(t, args); if (!is_constant(fn)) return false; - if (!m_env.get(const_name(fn)).is_inductive()) + if (!is_inductive(m_env, const_name(fn))) return false; if (!m_env.find(name{const_name(fn), "cases_on"}) || !m_env.find(get_eq_name())) return false; diff --git a/src/library/user_recursors.cpp b/src/library/user_recursors.cpp index 31933e5184..f00e3dfecd 100644 --- a/src/library/user_recursors.cpp +++ b/src/library/user_recursors.cpp @@ -333,7 +333,7 @@ typedef scoped_ext recursor_ext; environment add_user_recursor(environment const & env, name const & r, optional const & major_pos, bool persistent) { - if (env.get(r).is_recursor()) + if (is_recursor(env, r)) throw exception(sstream() << "invalid user defined recursor, '" << r << "' is a builtin recursor"); recursor_info info = mk_recursor_info(env, r, major_pos); return recursor_ext::add_entry(env, get_dummy_ios(), info, persistent); diff --git a/src/library/util.cpp b/src/library/util.cpp index 6040dc90b7..65dc55dd90 100644 --- a/src/library/util.cpp +++ b/src/library/util.cpp @@ -247,7 +247,7 @@ void get_constructor_names(environment const & env, name const & n, buffer optional is_constructor_app(environment const & env, expr const & e) { expr const & fn = get_app_fn(e); if (is_constant(fn)) { - if (env.get(const_name(fn)).is_constructor()) + if (is_constructor(env, const_name(fn))) return optional(const_name(fn)); } return optional();