Method apply

lean_py/z3/tactic.py:85–100

Apply this tactic to a goal via Pantograph.

(self, goal: Goal)

        self._name = name

    def apply(self, goal: Goal) -> ApplyResult:
        """Apply this tactic to a goal via Pantograph."""
        expr = goal.as_expr()
        k = _get_kernel()
        lib = k._lib

        ast = _wrap_free_vars(expr)
        z3_expr = _marshal_expr(lib, ast)
        lean_expr = lib.z3_compile(z3_expr)
        gs = k.goal_create_expr(lean_expr)

        result = gs.try_tactic(self._name)
        if result.ok and result.state is not None and result.state.is_solved():
            return ApplyResult([])  # proved
        # Tactic produced subgoals or failed
        return ApplyResult([goal])  # unchanged

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