Function z3_sys::Z3_mk_list_sort

pub unsafe extern "C" fn Z3_mk_list_sort(
    c: Z3_context, 
    name: Z3_symbol, 
    elem_sort: Z3_sort, 
    nil_decl: *mut Z3_func_decl, 
    is_nil_decl: *mut Z3_func_decl, 
    cons_decl: *mut Z3_func_decl, 
    is_cons_decl: *mut Z3_func_decl, 
    head_decl: *mut Z3_func_decl, 
    tail_decl: *mut Z3_func_decl
) -> Z3_sort

Create a list sort

A list sort over elem_sort This function declares the corresponding constructors and testers for lists.

• c: logical context
• name: name of the list sort.
• elem_sort: sort of list elements.
• nil_decl: declaration for the empty list.
• is_nil_decl: test for the empty list.
• cons_decl: declaration for a cons cell.
• is_cons_decl: cons cell test.
• head_decl: list head.
• tail_decl: list tail.