Method solver

lean_py/z3/tactic.py:102–104

Create a Solver that uses this tactic.

(self)

        return ApplyResult([goal])  # unchanged

    def solver(self):
        """Create a Solver that uses this tactic."""
        return Solver()

    def __repr__(self) -> str:
        return f"Tactic({self._name})"