Function z3_sys::Z3_mk_list_sort
source · 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
Expand description
Create a list sort
A list sort over elem_sort
This function declares the corresponding constructors and testers for lists.
c
: logical contextname
: 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.