Class FuncInterp

lean_py/z3/solver.py:1010–1033

Function interpretation in a model.

class FuncInterp:
    """Function interpretation in a model."""

    def __init__(self) -> None:
        pass

    def else_value(self) -> Any:
        raise NotImplementedError(
            "Model extraction not supported: Lean cannot produce counter-models"
        )

    def num_entries(self) -> int:
        return 0

    def entry(self, i: int) -> FuncEntry:
        raise NotImplementedError(
            "Model extraction not supported: Lean cannot produce counter-models"
        )

    def arity(self) -> int:
        return 0

    def as_list(self) -> list:
        return []


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