Method process

lean_py/kernel.py:381–386

Process Lean source code against the current environment. Returns a multi-line string of new constants per command, separated by ``\\n---\\n``.

(self, source: str)

        return s

    def process(self, source: str) -> str:
        """Process Lean source code against the current environment.

        Returns a multi-line string of new constants per command, separated by
        ``\\n---\\n``."""
        return self._lib.leanpy_kernel_frontend_process(source)

    def collect_sorrys(self, source: str) -> tuple[GoalState | None, str]:
        """Extract all `sorry` placeholders in ``source`` as a draftable