From a241bd332851aa6e8f8ecda4331d6ce5c2f2bdf3 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 12 Apr 2018 14:51:07 -0700
Subject: [PATCH] chore(kernel/type_checker): remove dead code

---
 src/kernel/type_checker.cpp | 9 ---------
 src/kernel/type_checker.h   | 3 ---
 2 files changed, 12 deletions(-)

diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp
index 761accb55a..8323da09c9 100644
--- a/src/kernel/type_checker.cpp
+++ b/src/kernel/type_checker.cpp
@@ -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");
diff --git a/src/kernel/type_checker.h b/src/kernel/type_checker.h
index f06b4cfb91..8c4d79dd67 100644
--- a/src/kernel/type_checker.h
+++ b/src/kernel/type_checker.h
@@ -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);