Documentation

Aesop.Tree.State

Marking Nodes As Proven/Unprovable/Irrelevant #

Irrelevant #

source
def Aesop.Goal.isIrrelevantNoCache (g : Goal) :
BaseIO Bool
Instances For
    source
    def Aesop.Rapp.isIrrelevantNoCache (r : Rapp) :
    BaseIO Bool
    Instances For
      source
      def Aesop.MVarCluster.isIrrelevantNoCache (c : MVarCluster) :
      BaseIO Bool
      Instances For
        source
        def Aesop.TreeRef.markSubtreeIrrelevant :
        TreeRef → BaseIO Unit
        Instances For
          source
          def Aesop.GoalRef.markSubtreeIrrelevant (gref : GoalRef) :
          BaseIO Unit
          Instances For
            source
            def Aesop.RappRef.markSubtreeIrrelevant (rref : RappRef) :
            BaseIO Unit
            Instances For
              source
              def Aesop.MVarClusterRef.markSubtreeIrrelevant (cref : MVarClusterRef) :
              BaseIO Unit
              Instances For

                Proven #

                source
                def Aesop.Goal.isProvenByNormalizationNoCache (g : Goal) :
                Bool
                Instances For
                  source
                  def Aesop.Goal.isProvenByRuleApplicationNoCache (g : Goal) :
                  BaseIO Bool
                  Instances For
                    source
                    def Aesop.Goal.isProvenNoCache (g : Goal) :
                    BaseIO Bool
                    Instances For
                      source
                      def Aesop.Rapp.isProvenNoCache (r : Rapp) :
                      BaseIO Bool
                      Instances For
                        source
                        def Aesop.MVarCluster.isProvenNoCache (c : MVarCluster) :
                        BaseIO Bool
                        Instances For
                          source
                          def Aesop.GoalRef.markProvenByNormalization (gref : GoalRef) :
                          BaseIO Unit
                          Instances For
                            source
                            def Aesop.RappRef.markProven (rref : RappRef) :
                            BaseIO Unit
                            Instances For

                              Unprovable #

                              source
                              def Aesop.Goal.isUnprovableNoCache (g : Goal) :
                              BaseIO Bool
                              Instances For
                                source
                                def Aesop.Rapp.isUnprovableNoCache (r : Rapp) :
                                BaseIO Bool
                                Instances For
                                  source
                                  def Aesop.MVarCluster.isUnprovableNoCache (c : MVarCluster) :
                                  BaseIO Bool
                                  Instances For
                                    source
                                    def Aesop.GoalRef.markUnprovable (gref : GoalRef) :
                                    BaseIO Unit
                                    Instances For
                                      source
                                      def Aesop.GoalRef.markForcedUnprovable (gref : GoalRef) :
                                      BaseIO Unit
                                      Instances For
                                        source
                                        def Aesop.GoalRef.checkAndMarkUnprovable (gref : GoalRef) :
                                        BaseIO Unit
                                        Instances For

                                          Uncached Node States #

                                          source
                                          def Aesop.Goal.stateNoCache (g : Goal) :
                                          BaseIO GoalState
                                          Instances For
                                            source
                                            def Aesop.Rapp.stateNoCache (r : Rapp) :
                                            BaseIO NodeState
                                            Instances For
                                              source
                                              def Aesop.MVarCluster.stateNoCache (c : MVarCluster) :
                                              BaseIO NodeState
                                              Instances For