From 7bf0011905d4466d8f67c1649cd31c30acca940e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 18 May 2014 13:15:44 -0700 Subject: [PATCH] feat(kernel/expr): add additional template for mk_app Signed-off-by: Leonardo de Moura --- src/kernel/expr.h | 1 + 1 file changed, 1 insertion(+) diff --git a/src/kernel/expr.h b/src/kernel/expr.h index eb912c9ce..875b31f98 100644 --- a/src/kernel/expr.h +++ b/src/kernel/expr.h @@ -434,6 +434,7 @@ inline expr mk_app(expr const & f, expr const & a) { return expr(new expr_app(f, expr mk_app(unsigned num_args, expr const * args); inline expr mk_app(std::initializer_list const & l) { return mk_app(l.size(), l.begin()); } template expr mk_app(T const & args) { return mk_app(args.size(), args.data()); } +template expr mk_app(expr const & f, T const & args) { return mk_app(f, args.size(), args.data()); } expr mk_rev_app(expr const & f, unsigned num_args, expr const * args); expr mk_rev_app(unsigned num_args, expr const * args); template expr mk_rev_app(T const & args) { return mk_rev_app(args.size(), args.data()); }