Function lambda_const 

pub fn lambda_const(bounds: &[&dyn Ast], body: &Dynamic) -> Array

Create a lambda expression.

• num_decls: Number of variables to be bound.
• sorts: Bound variable sorts.
• decl_names: Contains the names that the quantified formula uses for the bound variables.
• body: Expression body that contains bound variables of the same sorts as the sorts listed in the array sorts.

Examples

let input = Int::fresh_const("");
let lambda = lambda_const(
    &[&input],
    &Dynamic::from_ast(&Int::add(&[&input, &Int::from_i64(2)])),
);

solver.assert(
    &lambda.select_n(&[&Int::from_i64(1)]).as_int().unwrap()
        ._eq(&Int::from_i64(3))
);

assert_eq!(solver.check(), SatResult::Sat);

solver.assert(
    &lambda.select_n(&[&Int::from_i64(1)]).as_int().unwrap()
        ._eq(&Int::from_i64(2))
);

assert_eq!(solver.check(), SatResult::Unsat);