Documentation

Aesop.Tree.State

Marking Nodes As Proven/Unprovable/Irrelevant #

Irrelevant #

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

                              Proven #

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

                                                          Unprovable #

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

                                                                                  Uncached Node States #

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