Method goal_create

lean_py/kernel.py:341–345

Create a new goal state from a type expression string. Raises ``LeanError`` on parse / elaboration failure.

(self, type_str: str)

    # -- goal state ------------------------------------------------------

    def goal_create(self, type_str: str) -> GoalState:
        """Create a new goal state from a type expression string. Raises
        ``LeanError`` on parse / elaboration failure."""
        handle = self._lib.leanpy_kernel_goal_create(type_str)
        return GoalState(self, handle)

    def goal_create_expr(self, expr: Any) -> GoalState:
        """Create a new goal state from a ``Lean.Expr`` object. Raises