Function z3_sys::Z3_add_rec_def

pub unsafe extern "C" fn Z3_add_rec_def(
    c: Z3_context, 
    f: Z3_func_decl, 
    n: c_uint, 
    args: *mut Z3_ast, 
    body: Z3_ast
)

Define the body of a recursive function.

• c: logical context.
• f: function declaration.
• n: number of arguments to the function
• args: constants that are used as arguments to the recursive function in the definition.
• body: body of the recursive function

After declaring a recursive function or a collection of mutually recursive functions, use this function to provide the definition for the recursive function.

See also:

• Z3_mk_rec_func_decl