Function define_fun 

pub unsafe extern "C" fn define_fun(
    cvc5: *mut Solver,
    symbol: *const c_char,
    size: usize,
    vars: *const Term,
    sort: Sort,
    term: Term,
    global: bool,
) -> Term

Define n-ary function.

SMT-LIB:

\verbatim embed:rst:leading-asterisk .. code:: smtlib

(define-fun <function_def>)

\endverbatim

@param cvc5 The cvc5 solver instance. @param symbol The name of the function. @param size The number of parameters of the function. @param vars The parameters. @param sort The sort of the return value of this function. @param term The function body. @param global Determines whether this definition is global (i.e., persists when popping the context). @return The function.