[−][src]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.

See also: