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);