(self, goal: Goal)
| 122 | self._tactics = tactics |
| 123 | |
| 124 | def apply(self, goal: Goal) -> ApplyResult: |
| 125 | current = ApplyResult([goal]) |
| 126 | for tac in self._tactics: |
| 127 | next_subgoals: list[Goal] = [] |
| 128 | for sg in current._subgoals: |
| 129 | result = tac.apply(sg) |
| 130 | next_subgoals.extend(result._subgoals) |
| 131 | current = ApplyResult(next_subgoals) |
| 132 | if not current._subgoals: |
| 133 | break |
| 134 | return current |
| 135 | |
| 136 | |
| 137 | class _OrElseTactic(Tactic): |
nothing calls this directly
no test coverage detected