Method parse

lean_py/kernel.py:56–67

Parse the multi-line encoding produced by Lean's ``encodeTacticResult``.

(cls, encoded: str, kernel: Kernel, raw_state: Any)

    @classmethod
    def parse(cls, encoded: str, kernel: Kernel, raw_state: Any) -> TacticResult:
        """Parse the multi-line encoding produced by Lean's
        ``encodeTacticResult``."""
        if not encoded:
            return cls("failure", [], None)
        lines = encoded.split("\n")
        status = lines[0]
        messages = lines[1:] if len(lines) > 1 else []
        state = None
        if status == "success" and raw_state is not None:
            state = GoalState(kernel, raw_state)
        return cls(status, messages, state)


class GoalState: