Equivalent to ``let : := ?``.
(self, binder_name: str, type_str: str)
| 128 | return TacticResult.parse(encoded, self._kernel, next_state) |
| 129 | |
| 130 | def try_let(self, binder_name: str, type_str: str) -> TacticResult: |
| 131 | """Equivalent to ``let <binder_name> : <type_str> := ?``.""" |
| 132 | encoded, next_state = self._kernel._lib.leanpy_kernel_goal_try_let( |
| 133 | self._handle, |
| 134 | binder_name, |
| 135 | type_str, |
| 136 | ) |
| 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>``.""" |