Method goal_create_expr

lean_py/kernel.py:347–351

Create a new goal state from a ``Lean.Expr`` object. Raises ``LeanError`` on type-check failure.

(self, expr: Any)

        return GoalState(self, handle)

    def goal_create_expr(self, expr: Any) -> GoalState:
        """Create a new goal state from a ``Lean.Expr`` object. Raises
        ``LeanError`` on type-check failure."""
        handle = self._lib.z3_goal_create_expr(expr)
        return GoalState(self, handle)

    def goal_unpickle(self, path: str) -> GoalState:
        """Load a goal state previously serialised with :meth:`GoalState.pickle`."""