Function Lambda

lean_py/z3/core.py:2184–2201

Build a lambda expression (maps to Lean lambda).

(vars: ExprRef | Sequence[ExprRef], body: ExprRef)

def Lambda(vars: ExprRef | Sequence[ExprRef], body: ExprRef) -> ExprRef:
    """Build a lambda expression (maps to Lean lambda)."""
    vs = [vars] if isinstance(vars, ExprRef) else list(vars)
    bound_names = frozenset(
        (v._ast.name, v._sort._ast_sort) for v in vs if isinstance(v._ast, _AstVar)
    )
    free = body._vars - bound_names
    for v in vs:
        free = free | v._vars - bound_names

    ast: ASTNode = body._ast
    for v in reversed(vs):
        ast = LambdaNode(
            name=v._ast.name if isinstance(v._ast, _AstVar) else str(v._ast),
            sort=v._sort._ast_sort,
            body=ast,
        )
    return ExprRef(ast, body._sort, free)


# ---------------------------------------------------------------------------