Function z3_sys::Z3_mk_datatypes

pub unsafe extern "C" fn Z3_mk_datatypes(
    c: Z3_context, 
    num_sorts: c_uint, 
    sort_names: *const Z3_symbol, 
    sorts: *mut Z3_sort, 
    constructor_lists: *mut Z3_constructor_list
)

Create mutually recursive datatypes.

• c: logical context.
• num_sorts: number of datatype sorts.
• sort_names: names of datatype sorts.
• sorts: array of datatype sorts.
• constructor_lists: list of constructors, one list per sort.