mk_lambda_const method

Z3_ast mk_lambda_const(
  1. Z3_context c,
  2. int num_bound,
  3. Pointer<Z3_app> bound,
  4. Z3_ast body,
)

\brief Create a lambda expression using a list of constants that form the set of bound variables

\param c logical context. \param num_bound number of constants to be abstracted into bound variables. \param bound array of constants to be abstracted into bound variables. \param body the body of the lambda expression.

\sa Z3_mk_bound \sa Z3_mk_forall \sa Z3_mk_lambda

def_API('Z3_mk_lambda_const', AST, (_in(CONTEXT), _in(UINT), _in_array(1, APP), _in(AST)))

Implementation

Z3_ast mk_lambda_const(
  Z3_context c,
  int num_bound,
  ffi.Pointer<Z3_app> bound,
  Z3_ast body,
) {
  return _mk_lambda_const(
    c,
    num_bound,
    bound,
    body,
  );
}