(self, goal: Goal)
| 162 | self._max = max_iter |
| 163 | |
| 164 | def apply(self, goal: Goal) -> ApplyResult: |
| 165 | current = ApplyResult([goal]) |
| 166 | for _ in range(self._max): |
| 167 | next_subgoals: list[Goal] = [] |
| 168 | changed = False |
| 169 | for sg in current._subgoals: |
| 170 | result = self._tactic.apply(sg) |
| 171 | if len(result) == 0 or result._subgoals != [sg]: |
| 172 | changed = True |
| 173 | next_subgoals.extend(result._subgoals) |
| 174 | current = ApplyResult(next_subgoals) |
| 175 | if not changed or not current._subgoals: |
| 176 | break |
| 177 | return current |
| 178 | |
| 179 | |
| 180 | def Then(*tactics: Tactic) -> Tactic: |
nothing calls this directly
no test coverage detected