Equivalent to ``let := ``.
(self, binder_name: str, expr_str: str)
| 137 | return TacticResult.parse(encoded, self._kernel, next_state) |
| 138 | |
| 139 | def try_define(self, binder_name: str, expr_str: str) -> TacticResult: |
| 140 | """Equivalent to ``let <binder_name> := <expr_str>``.""" |
| 141 | encoded, next_state = self._kernel._lib.leanpy_kernel_goal_try_define( |
| 142 | self._handle, |
| 143 | binder_name, |
| 144 | expr_str, |
| 145 | ) |
| 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, |