Method else_value

lean_py/z3/solver.py:1016–1019

(self)

        pass

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

    def num_entries(self) -> int:
        return 0