parameters: (self, tactic_application: TacticApplication)
docstring: Mark the proof search node closed.
  
      This function assumes that we have a fully closed subtree on one of
      the TacticApplications in successful_attempts. Assertion will fail
      if this is not the case.
  
      Args:
        tactic_application: The TacticApplication that has lead to a proof. This
          parameter is only used for verifying that the node is really closed.
          Assertions will fail if that's not the case.
docstring_summary: Mark the proof search node closed.
docstring_tokens: Mark the proof search node closed .
function: def mark_closed(self, tactic_application: TacticApplication):
      """Mark the proof search node closed.
  
      This function assumes that we have a fully closed subtree on one of
      the TacticApplications in successful_attempts. Assertion will fail
      if this is not the case.
  
      Args:
        tactic_application: The TacticApplication that has lead to a proof. This
          parameter is only used for verifying that the node is really closed.
          Assertions will fail if that's not the case.
      """
      assert self.closed is not None
      if self.closed:
        return
      # Check that the tactic_application belongs to this node.
      assert tactic_application.parent.index == self.index
      # Make sure that all subgoals are really closed.
      for subgoal in tactic_application.subgoals:
        assert subgoal.closed
      self.closed = True
      # Now, we don't want to close this goal again. We ignore it
      # for all further attempts.
      self.ignored = True
      # For all other non-closed tactic application, ignore the children
      # if they don't need to be closed as other subgoals.
      for tac_app in self.successful_attempts:
        if not tac_app.closed:
          for subgoal in tac_app.subgoals:
            # Mark all subgoals in the other proof attempts as ignore, they
            # have become useless for closing this goal.
            subgoal.update_ignore()
      # Note that update_closed does not necessarily close the
      # parent. Only, if all of their subgoals are closed.
      # In general, we have a recursive call, that might mark
      # all the closed (sub-)goals closed in the relevant part
      # of the search tree, if they got proved.
      for subgoal_ref in self.parents:
        subgoal_ref.tactic_application.update_closed()
function_tokens: def mark_closed ( self , tactic_application : TacticApplication ) : assert self . closed is not None if self . closed : return # Check that the tactic_application belongs to this node. assert tactic_application . parent . index == self . index # Make sure that all subgoals are really closed. for subgoal in tactic_application . subgoals : assert subgoal . closed self . closed = True # Now, we don't want to close this goal again. We ignore it # for all further attempts. self . ignored = True # For all other non-closed tactic application, ignore the children # if they don't need to be closed as other subgoals. for tac_app in self . successful_attempts : if not tac_app . closed : for subgoal in tac_app . subgoals : # Mark all subgoals in the other proof attempts as ignore, they # have become useless for closing this goal. subgoal . update_ignore ( ) # Note that update_closed does not necessarily close the # parent. Only, if all of their subgoals are closed. # In general, we have a recursive call, that might mark # all the closed (sub-)goals closed in the relevant part # of the search tree, if they got proved. for subgoal_ref in self . parents : subgoal_ref . tactic_application . update_closed ( )