Method eval

lean_py/z3/solver.py:518–521

(self, t: Any, model_completion: bool = False)

        )

    def eval(self, t: Any, model_completion: bool = False) -> Any:
        raise NotImplementedError(
            "Model extraction not supported: Lean cannot produce counter-models"
        )

    evaluate = eval