Function Function

lean_py/z3/core.py:1037–1045

Declare an uninterpreted function. ``Function('f', IntSort(), IntSort(), BoolSort())`` declares ``f : Int -> Int -> Prop``.

(name: str, *sorts: SortRef)

def Function(name: str, *sorts: SortRef) -> FuncDeclRef:
    """Declare an uninterpreted function.

    ``Function('f', IntSort(), IntSort(), BoolSort())`` declares
    ``f : Int -> Int -> Prop``.
    """
    if len(sorts) < 2:
        raise TypeError("Function needs at least a domain and range sort")
    return FuncDeclRef(name, tuple(sorts[:-1]), sorts[-1])


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