parameters: (self)
docstring: Mark this tactic-application failed if any of the subgoals has failed.
  
      Note that having "failed" is a soft condition, not a definitive one. Right
      now, the hard-coded behavior is to "fail" if no tactic could is applied
      in a way that changes the goal without producing error. However, this
      behavior might be overridden.
docstring_summary: Mark this tactic-application failed if any of the subgoals has failed.
docstring_tokens: Mark this tactic - application failed if any of the subgoals has failed .
function: def mark_failed(self):
      """Mark this tactic-application failed if any of the subgoals has failed.
  
      Note that having "failed" is a soft condition, not a definitive one. Right
      now, the hard-coded behavior is to "fail" if no tactic could is applied
      in a way that changes the goal without producing error. However, this
      behavior might be overridden.
      """
      if self.failed:
        # Nothing to do, we are already marked as a failure.
        # Make sure that we have not marked this node closed. That would be a
        # contradiction.
        assert not self.closed
        return
      for subgoal in self.subgoals:
        if subgoal.failed:
          # We have found a failing subgoal.
          # Make sure that we have not marked this node closed. That would be a
          # contradiction.
          assert not self.closed
          # This tactic application is failed since we can't close it anymore.
          self.failed = True
          # Update the parent node to be failed if all of its tactic applications
          # have failed.
          self.parent.update_failed()
          # We would like to mark all non-failing sibling nodes and their
          # descendants useless if they have not chance of contributing to closing
          # any other goal.
          for sibling in self.subgoals:
            sibling.update_ignore()
          # Don't do duplicated work.
          return
function_tokens: def mark_failed ( self ) : if self . failed : # Nothing to do, we are already marked as a failure. # Make sure that we have not marked this node closed. That would be a # contradiction. assert not self . closed return for subgoal in self . subgoals : if subgoal . failed : # We have found a failing subgoal. # Make sure that we have not marked this node closed. That would be a # contradiction. assert not self . closed # This tactic application is failed since we can't close it anymore. self . failed = True # Update the parent node to be failed if all of its tactic applications # have failed. self . parent . update_failed ( ) # We would like to mark all non-failing sibling nodes and their # descendants useless if they have not chance of contributing to closing # any other goal. for sibling in self . subgoals : sibling . update_ignore ( ) # Don't do duplicated work. return