From b6472d043ef3a381620acee77587dbbca852d677 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 14 Aug 2016 16:16:03 -0700 Subject: [PATCH] feat(kernel/instantiate): add helper function --- src/kernel/instantiate.h | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/kernel/instantiate.h b/src/kernel/instantiate.h index beb4e92928..dc4885dbd5 100644 --- a/src/kernel/instantiate.h +++ b/src/kernel/instantiate.h @@ -20,6 +20,9 @@ expr instantiate(expr const & e, expr const & s); /** \brief Replace the free variables with indices 0, ..., n-1 with s[n-1], ..., s[0] in e. */ expr instantiate_rev(expr const & e, unsigned n, expr const * s); +inline expr instantiate_rev(expr const & e, buffer const & s) { + return instantiate_rev(e, s.size(), s.data()); +} expr apply_beta(expr f, unsigned num_args, expr const * args); bool is_head_beta(expr const & t);