Function z3_sys::Z3_mk_lambda_const [−][src]
pub unsafe extern "C" fn Z3_mk_lambda_const(
c: Z3_context,
num_bound: c_uint,
bound: *const Z3_app,
body: Z3_ast
) -> Z3_ast
Expand description
Create a lambda expression using a list of constants that form the set of bound variables
c
: logical context.num_bound
: number of constants to be abstracted into bound variables.bound
: array of constants to be abstracted into bound variables.body
: the body of the lambda expression.