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

chore(kernel/type_checker): remove dead code

Browse source
This commit is contained in:
Leonardo de Moura 2018-04-12 14:51:07 -07:00
parent 5b530f24aa
commit a241bd3328
2 changed files with 0 additions and 12 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/kernel/type_checker.cpp
View file

@ -278,15 +278,6 @@ optional<expr> type_checker::norm_ext(expr const & e) {
return m_env.norm_ext()(e, *this);
}
/** \brief Return true if \c e may be reduced later after metavariables are instantiated. */
optional<expr> type_checker::is_stuck(expr const & e) {
if (is_meta(e)) {
return some_expr(e);
} else {
return m_env.norm_ext().is_stuck(e, *this);
}
}
/** \brief Weak head normal form core procedure. It does not perform delta reduction nor normalization extensions. */
expr type_checker::whnf_core(expr const & e) {
check_system("whnf");

3
src/kernel/type_checker.h
View file

@ -131,9 +131,6 @@ public:
optional<expr> expand_macro(expr const & m);
/** \brief Return a metavariable that may be stucking the \c e's reduction. */
virtual optional<expr> is_stuck(expr const & e);
template<typename F>
typename std::result_of<F()>::type with_params(level_param_names const & ps, F && f) {
flet<level_param_names const *> updt(m_params, &ps);