Opaque handle to a Lean ``GoalState``. Methods dispatch back into the underlying Lean library.
| 68 | |
| 69 | |
| 70 | class GoalState: |
| 71 | """Opaque handle to a Lean ``GoalState``. Methods dispatch back into the |
| 72 | underlying Lean library.""" |
| 73 | |
| 74 | __slots__ = ("_kernel", "_handle") |
| 75 | |
| 76 | def __init__(self, kernel: Kernel, handle: Any) -> None: |
| 77 | self._kernel = kernel |
| 78 | self._handle = handle |
| 79 | |
| 80 | @property |
| 81 | def handle(self) -> Any: |
| 82 | return self._handle |
| 83 | |
| 84 | def is_solved(self) -> bool: |
| 85 | return self._kernel._lib.leanpy_kernel_goal_is_solved(self._handle) |
| 86 | |
| 87 | def n_goals(self) -> int: |
| 88 | return int(self._kernel._lib.leanpy_kernel_goal_n_goals(self._handle)) |
| 89 | |
| 90 | def main_goal_name(self) -> str: |
| 91 | return self._kernel._lib.leanpy_kernel_goal_main_goal_name(self._handle) |
| 92 | |
| 93 | def root_expr(self) -> str: |
| 94 | return self._kernel._lib.leanpy_kernel_goal_root_expr(self._handle) |
| 95 | |
| 96 | def pretty(self) -> str: |
| 97 | return self._kernel._lib.leanpy_kernel_goal_pretty(self._handle) |
| 98 | |
| 99 | def try_tactic(self, tactic: str) -> TacticResult: |
| 100 | encoded, next_state = self._kernel._lib.leanpy_kernel_goal_try_tactic(self._handle, tactic) |
| 101 | return TacticResult.parse(encoded, self._kernel, next_state) |
| 102 | |
| 103 | def try_assign(self, expr: str) -> TacticResult: |
| 104 | encoded, next_state = self._kernel._lib.leanpy_kernel_goal_try_assign(self._handle, expr) |
| 105 | return TacticResult.parse(encoded, self._kernel, next_state) |
| 106 | |
| 107 | def conv_enter(self) -> TacticResult: |
| 108 | encoded, next_state = self._kernel._lib.leanpy_kernel_goal_conv_enter(self._handle) |
| 109 | return TacticResult.parse(encoded, self._kernel, next_state) |
| 110 | |
| 111 | def calc_enter(self) -> TacticResult: |
| 112 | encoded, next_state = self._kernel._lib.leanpy_kernel_goal_calc_enter(self._handle) |
| 113 | return TacticResult.parse(encoded, self._kernel, next_state) |
| 114 | |
| 115 | def fragment_exit(self) -> TacticResult: |
| 116 | encoded, next_state = self._kernel._lib.leanpy_kernel_goal_fragment_exit(self._handle) |
| 117 | return TacticResult.parse(encoded, self._kernel, next_state) |
| 118 | |
| 119 | # ---- prograde tactics -------------------------------------------------- |
| 120 | |
| 121 | def try_have(self, binder_name: str, type_str: str) -> TacticResult: |
| 122 | """Equivalent to ``have <binder_name> : <type_str> := ?``.""" |
| 123 | encoded, next_state = self._kernel._lib.leanpy_kernel_goal_try_have( |
| 124 | self._handle, |
| 125 | binder_name, |
| 126 | type_str, |
| 127 | ) |
no outgoing calls
no test coverage detected