(self, branch: GoalState)
| 196 | return GoalState(self._kernel, next_state) |
| 197 | |
| 198 | def continue_with(self, branch: GoalState) -> GoalState: |
| 199 | next_state, err = self._kernel._lib.leanpy_kernel_goal_continue( |
| 200 | self._handle, |
| 201 | branch._handle, |
| 202 | ) |
| 203 | if err: |
| 204 | raise RuntimeError(f"continue failed: {err}") |
| 205 | return GoalState(self._kernel, next_state) |
| 206 | |
| 207 | def replay(self, src: GoalState, src_prime: GoalState) -> GoalState: |
| 208 | """Merge differential ``src → src_prime`` onto ``self`` (the dst).""" |