From 6dedb480ecfc5f4be0c8bc4cb8201d0a7740066d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 16 May 2014 17:47:04 -0700 Subject: [PATCH] fix(kernel/abstract): bug in abstract for telescopes Signed-off-by: Leonardo de Moura --- src/kernel/abstract.cpp | 5 +++-- src/kernel/abstract.h | 2 ++ 2 files changed, 5 insertions(+), 2 deletions(-) diff --git a/src/kernel/abstract.cpp b/src/kernel/abstract.cpp index b3df33cc6..41f187f69 100644 --- a/src/kernel/abstract.cpp +++ b/src/kernel/abstract.cpp @@ -26,14 +26,15 @@ 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(), i, 1, &s)), - abstract(head(t), s, i+1)); + return telescope(b.update_type(abstract(b.get_type(), s, i)), + abstract(tail(t), s, i+1)); } } diff --git a/src/kernel/abstract.h b/src/kernel/abstract.h index ea7058bd2..53531c432 100644 --- a/src/kernel/abstract.h +++ b/src/kernel/abstract.h @@ -19,6 +19,8 @@ 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 const & l) { return abstract(e, l.size(), l.begin()); } +/** \brief Replace s with variable #i in the given telescope. \pre s is closed */ +expr abstract(expr const & e, expr const & s, unsigned i); /** \brief Replace s with variable #i in the given telescope.