max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore(library/type_context): remove reduce_large_elim_recursor

Browse source
This commit is contained in:
Leonardo de Moura 2018-09-03 16:21:00 -07:00
parent 799c133326
commit d54b86d16b
2 changed files with 0 additions and 20 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

19
src/library/type_context.cpp
View file

@ -730,18 +730,6 @@ optional<expr> type_context_old::reduce_aux_recursor(expr const & e) {
}
}
optional<expr> type_context_old::reduce_large_elim_recursor(expr const & e) {
expr const & f = get_app_fn(e);
if (!is_constant(f))
return none_expr();
auto & fn = const_name(f);
if (fn == get_acc_rec_name()) {
transparency_scope scope(*this, transparency_mode::All);
return norm_ext(e);
}
return none_expr();
}
bool type_context_old::use_zeta() const {
return m_zeta;
}
@ -751,8 +739,6 @@ optional<expr> type_context_old::reduce_recursor(expr const & e) {
return r;
if (auto r = reduce_aux_recursor(e))
return r;
if (auto r = reduce_large_elim_recursor(e))
return r;
return none_expr();
}
@ -849,11 +835,6 @@ expr type_context_old::whnf_core(expr const & e0, bool proj_reduce) {
continue;
}
if (auto r = reduce_large_elim_recursor(e)) {
e = *r;
continue;
}
return e;
} else {
e = mk_rev_app(f, args.size(), args.data());

1
src/library/type_context.h
View file

@ -683,7 +683,6 @@ public:
This method is useful when we want to normalize the expression until we get a particular symbol as the head symbol. */
expr whnf_head_pred(expr const & e, std::function<bool(expr const &)> const & pred); // NOLINT
optional<expr> reduce_aux_recursor(expr const & e);
optional<expr> reduce_large_elim_recursor(expr const & e);
optional<expr> reduce_projection(expr const & e);
optional<expr> reduce_proj(expr const & e);
optional<expr> norm_ext(expr const & e);