MCPcopy Create free account
hub / github.com/BasisResearch/lean.py / goal_unpickle

Method goal_unpickle

lean_py/kernel.py:353–358  ·  view source on GitHub ↗

Load a goal state previously serialised with :meth:`GoalState.pickle`.

(self, path: str)

Source from the content-addressed store, hash-verified

351 return GoalState(self, handle)
352
353 def goal_unpickle(self, path: str) -> GoalState:
354 """Load a goal state previously serialised with :meth:`GoalState.pickle`."""
355 handle, err = self._lib.leanpy_kernel_goal_unpickle(str(path))
356 if err:
357 raise RuntimeError(f"goal unpickle failed: {err}")
358 return GoalState(self, handle)
359
360 # -- environment serialisation ---------------------------------------
361

Callers 1

Calls 1

GoalStateClass · 0.85

Tested by 1