From a0fb3eb2f92472b44ce9a03fc80ef592bb96e47e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 9 Sep 2016 17:43:42 -0700 Subject: [PATCH] feat(library/equations_compiler/equations): add helper function --- src/library/equations_compiler/equations.h | 1 + 1 file changed, 1 insertion(+) diff --git a/src/library/equations_compiler/equations.h b/src/library/equations_compiler/equations.h index 6b041d05c2..5c54e9081b 100644 --- a/src/library/equations_compiler/equations.h +++ b/src/library/equations_compiler/equations.h @@ -57,6 +57,7 @@ expr const & equations_wf_rel(expr const & e); the \c n resulting functions (and their types) with an \c equations_result macro. */ bool is_equations_result(expr const & e); expr mk_equations_result(unsigned n, expr const * rs); +inline expr mk_equations_result(expr const & e) { return mk_equations_result(1, &e); } unsigned get_equations_result_size(expr const & e); expr const & get_equations_result(expr const & e, unsigned i);