Method model

lean_py/z3/solver.py:596–599

(self)

        return unknown

    def model(self) -> ModelRef:
        raise NotImplementedError(
            "Model extraction not supported: Lean is a proof checker, not an SMT solver"
        )

    def assertions(self) -> list[BoolRef]:
        return list(self._assertions)