Class FuncEntry

lean_py/z3/solver.py:987–1007

A single entry in a function interpretation.

class FuncEntry:
    """A single entry in a function interpretation."""

    def __init__(self) -> None:
        pass

    def num_args(self) -> int:
        return 0

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

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

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


class FuncInterp: