Substitute the goal with an expression that may contain sorrys, leaving the sorrys as fresh subgoals.
(self, expr_str: str)
| 146 | return TacticResult.parse(encoded, self._kernel, next_state) |
| 147 | |
| 148 | def try_draft(self, expr_str: str) -> TacticResult: |
| 149 | """Substitute the goal with an expression that may contain sorrys, |
| 150 | leaving the sorrys as fresh subgoals.""" |
| 151 | encoded, next_state = self._kernel._lib.leanpy_kernel_goal_try_draft( |
| 152 | self._handle, |
| 153 | expr_str, |
| 154 | ) |
| 155 | return TacticResult.parse(encoded, self._kernel, next_state) |
| 156 | |
| 157 | # ---- introspection ----------------------------------------------------- |
| 158 |