refactor(kernel): remove telescope type, and procedures

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/kernel/abstract.cpp

@@ -28,19 +28,6 @@ expr abstract(expr const & e, unsigned s, unsigned n, expr const * subst) {
 expr abstract(expr const & e, unsigned n, expr const * subst) { return abstract(e, 0, n, subst); }
 expr abstract(expr const & e, expr const & s, unsigned i) { return abstract(e, i, 1, &s); }
 
-telescope abstract(telescope const & t, expr const & s, unsigned i) {
-    if (is_nil(t)) {
-        return t;
-    } else {
-        binder const & b = head(t);
-        return telescope(b.update_type(abstract(b.get_type(), s, i)),
-                         abstract(tail(t), s, i+1));
-    }
-}
-
-telescope abstract(telescope const & t, expr const & s) { return abstract(t, s, 0); }
-
-
 expr abstract_p(expr const & e, unsigned n, expr const * s) {
     lean_assert(std::all_of(s, s+n, closed));
     return replace(e, [=](expr const & e, unsigned offset) -> optional<expr> {

src/kernel/abstract.h

@@ -19,17 +19,9 @@ namespace lean {
 expr abstract(expr const & e, unsigned n, expr const * s);
 inline expr abstract(expr const & e, expr const & s) { return abstract(e, 1, &s); }
 inline expr abstract(expr const & e, std::initializer_list<expr> const & l) { return abstract(e, l.size(), l.begin()); }
-/** \brief Replace s with variable #i in the given telescope. \pre s is closed */
+/** \brief Replace s with variable #i in the given expression. \pre s is closed */
 expr abstract(expr const & e, expr const & s, unsigned i);
 
-/**
-    \brief Replace s with variable #i in the given telescope.
-    \pre s is closed
-*/
-telescope abstract(telescope const & t, expr const & s, unsigned i);
-/** \brief Replace s with variable #0 in the given telescope. */
-telescope abstract(telescope const & t, expr const & s);
-
 /**
    \brief Replace the expressions s[0], ..., s[n-1] in e with var(n-1), ..., var(0).
 

src/kernel/expr.h

@@ -267,9 +267,6 @@ public:
     binder update_type(expr const & t) const { return binder(m_name, t, m_info); }
 };
 
-// Remark: in a telescope T, variable 0 is the last element of the list, and head(T) is variable #(length(T) - 1)
-typedef list<binder> telescope;
-
 /** \brief Lambda and Pi expressions */
 class expr_binding : public expr_composite {
     binder           m_binder;

src/kernel/instantiate.cpp

@@ -40,17 +40,6 @@ expr instantiate(expr const & e, std::initializer_list<expr> const & l) {  retur
 expr instantiate(expr const & e, unsigned i, expr const & s) { return instantiate(e, i, 1, &s); }
 expr instantiate(expr const & e, expr const & s) { return instantiate(e, 0, s); }
 
-telescope instantiate(telescope const & t, unsigned i, expr const & s) {
-    if (is_nil(t)) {
-        return t;
-    } else {
-        binder const & b = head(t);
-        return telescope(b.update_type(instantiate(b.get_type(), i, s)),
-                         instantiate(tail(t), i+1, s));
-    }
-}
-telescope instantiate(telescope const & t, expr const & s) { return instantiate(t, s); }
-
 bool is_head_beta(expr const & t) {
     expr const * it = &t;
     while (is_app(*it)) {

src/kernel/instantiate.h

@@ -18,11 +18,6 @@ expr instantiate(expr const & e, unsigned i, expr const & s);
 /** \brief Replace free variable \c 0 with \c s in \c e. */
 expr instantiate(expr const & e, expr const & s);
 
-/** \brief Replace free variable \c i with \c s in the telescope t. */
-telescope instantiate(telescope const & t, unsigned i, expr const & s);
-/** \brief Replace free variable \c 0 with \c s in the telescope t. */
-telescope instantiate(telescope const & t, expr const & s);
-
 expr apply_beta(expr f, unsigned num_args, expr const * args);
 bool is_head_beta(expr const & t);
 expr head_beta_reduce(expr const & t);