Documentation

Aesop.Tree.Data

Node IDs #

structure Aesop.GoalId :
Instances For
    Equations
      Instances For
        Equations
          Instances For
            Equations
              Instances For
                Equations
                  Instances For
                    instance Aesop.GoalId.instDecidableRelLt :
                    DecidableRel fun (x1 x2 : GoalId) => x1 < x2
                    Equations

                      Rule Application IDs #

                      structure Aesop.RappId :
                      Instances For
                        Equations
                          Instances For
                            Equations
                              Instances For
                                Equations
                                  Instances For
                                    Equations
                                      Instances For
                                        instance Aesop.RappId.instDecidableRelLt :
                                        DecidableRel fun (x1 x2 : RappId) => x1 < x2
                                        Equations

                                          Iterations #

                                          Equations
                                            Instances For
                                              @[inline]
                                              Equations
                                                Instances For
                                                  @[inline]
                                                  Equations
                                                    Instances For
                                                      Equations
                                                        Instances For
                                                          Equations
                                                            Equations

                                                              The Tree #

                                                              At each point during the search, every node of the tree (goal, rapp or mvar cluster) is in one of these states:

                                                              • proven: the node is proven.
                                                              • unprovable: the node is unprovable, i.e. it will never be proven regardless of any future expansions that might be performed.
                                                              • unknown: neither of the above.

                                                              Every node starts in the unknown state and may later become either proven or unprovable. After this, the state does not change any more.

                                                              Instances For
                                                                Equations
                                                                  Instances For
                                                                    Equations
                                                                      Instances For
                                                                        Equations
                                                                          Instances For
                                                                            Equations
                                                                              Instances For
                                                                                Equations
                                                                                  Instances For

                                                                                    A refinement of the NodeState, distinguishing between goals proven during normalisation and goals proven by a child rule application.

                                                                                    Instances For
                                                                                      Equations
                                                                                        Instances For
                                                                                          Equations
                                                                                            Instances For
                                                                                              Equations
                                                                                                Instances For
                                                                                                  Equations
                                                                                                    Instances For
                                                                                                      Equations
                                                                                                        Instances For

                                                                                                          A goal G can be added to the tree for three reasons:

                                                                                                          1. G was produced by its parent rule as a subgoal. This is the most common reason.
                                                                                                          2. G was copied because it contains some metavariables which were assigned by its parent rule. In this case, we record goal of which G is a copy. We also record the representative of the equivalence class of goals which are copies of each other. E.g. if goal 1 is copied to goal 2 and goal 2 is copied to goal 3, they are all part of the equivalence class with representative 1.
                                                                                                          Instances For
                                                                                                            Equations
                                                                                                              Instances For
                                                                                                                structure Aesop.GoalData (Rapp MVarCluster : Type) :
                                                                                                                Instances For
                                                                                                                  instance Aesop.instNonemptyGoalData {Rapp✝ MVarCluster✝ : Type} [Nonempty MVarCluster✝] :
                                                                                                                  Nonempty (GoalData Rapp✝ MVarCluster✝)
                                                                                                                  structure Aesop.MVarClusterData (Goal Rapp : Type) :
                                                                                                                  Instances For
                                                                                                                    instance Aesop.instInhabitedMVarClusterData {a✝ a✝¹ : Type} :
                                                                                                                    Equations
                                                                                                                      structure Aesop.RappData (Goal MVarCluster : Type) :
                                                                                                                      Instances For
                                                                                                                        instance Aesop.instNonemptyRappData {Goal✝ : Type} [Nonempty Goal✝] {MVarCluster✝ : Type} :
                                                                                                                        Nonempty (RappData Goal✝ MVarCluster✝)
                                                                                                                        structure Aesop.TreeSpec :
                                                                                                                        Instances For
                                                                                                                          Equations
                                                                                                                            Instances For
                                                                                                                              @[implemented_by Aesop.treeImpl]
                                                                                                                              Equations
                                                                                                                                Instances For
                                                                                                                                  Equations
                                                                                                                                    Instances For
                                                                                                                                      Equations
                                                                                                                                        Instances For
                                                                                                                                          @[reducible, inline]
                                                                                                                                          Equations
                                                                                                                                            Instances For
                                                                                                                                              @[reducible, inline]
                                                                                                                                              Equations
                                                                                                                                                Instances For
                                                                                                                                                  @[reducible, inline]
                                                                                                                                                  Equations
                                                                                                                                                    Instances For
                                                                                                                                                      @[inline]
                                                                                                                                                      Equations
                                                                                                                                                        Instances For
                                                                                                                                                          @[inline]
                                                                                                                                                          Equations
                                                                                                                                                            Instances For
                                                                                                                                                              @[inline]
                                                                                                                                                              Equations
                                                                                                                                                                Instances For
                                                                                                                                                                  @[inline]
                                                                                                                                                                  Equations
                                                                                                                                                                    Instances For
                                                                                                                                                                      @[inline]
                                                                                                                                                                      Equations
                                                                                                                                                                        Instances For
                                                                                                                                                                          @[inline]
                                                                                                                                                                          Equations
                                                                                                                                                                            Instances For
                                                                                                                                                                              @[inline]
                                                                                                                                                                              Equations
                                                                                                                                                                                Instances For
                                                                                                                                                                                  @[inline]
                                                                                                                                                                                  Equations
                                                                                                                                                                                    Instances For
                                                                                                                                                                                      @[inline]
                                                                                                                                                                                      Equations
                                                                                                                                                                                        Instances For
                                                                                                                                                                                          @[inline]
                                                                                                                                                                                          Equations
                                                                                                                                                                                            Instances For
                                                                                                                                                                                              @[inline]
                                                                                                                                                                                              Equations
                                                                                                                                                                                                Instances For
                                                                                                                                                                                                  @[inline]
                                                                                                                                                                                                  Equations
                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                      @[inline]
                                                                                                                                                                                                      Equations
                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                          @[inline]
                                                                                                                                                                                                          Equations
                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                              @[inline]
                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                  @[inline]
                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                      @[inline]
                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                                          @[inline]
                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                                              @[inline]
                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                                  @[inline]
                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                                      @[inline]
                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                                                          @[inline]
                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                                                              @[inline]
                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                                                  @[inline]
                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                                                      @[inline]
                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                                                                          @[inline]
                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                                                                              @[inline]
                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                                                                  @[inline]
                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                                                                      @[inline]
                                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                                                                                          @[inline]
                                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                                                                                              @[inline]
                                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                                                                                  @[inline]
                                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                                                                                      @[inline]
                                                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                                                                                                          @[inline]
                                                                                                                                                                                                                                                                                          def Aesop.Goal.setId (id : GoalId) (g : Goal) :
                                                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                                                                                                              @[inline]
                                                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                                                                                                  @[inline]
                                                                                                                                                                                                                                                                                                  def Aesop.Goal.setChildren (children : Array RappRef) (g : Goal) :
                                                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                                                                                                      @[inline]
                                                                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                                                                                                                          @[inline]
                                                                                                                                                                                                                                                                                                          def Aesop.Goal.setDepth (depth : Nat) (g : Goal) :
                                                                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                                                                                                                              @[inline]
                                                                                                                                                                                                                                                                                                              def Aesop.Goal.setIsIrrelevant (isIrrelevant : Bool) (g : Goal) :
                                                                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                                                                                                                  @[inline]
                                                                                                                                                                                                                                                                                                                  def Aesop.Goal.setIsForcedUnprovable (isForcedUnprovable : Bool) (g : Goal) :
                                                                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                                                                                                                      @[inline]
                                                                                                                                                                                                                                                                                                                      def Aesop.Goal.setPreNormGoal (preNormGoal : Lean.MVarId) (g : Goal) :
                                                                                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                                                                                                                                          @[inline]
                                                                                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                                                                                                                                              @[inline]
                                                                                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                                                                                                                                  @[inline]
                                                                                                                                                                                                                                                                                                                                  def Aesop.Goal.setForwardState (forwardState : ForwardState) (g : Goal) :
                                                                                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                                                                                                                                      @[inline]
                                                                                                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                                                                                                                                                          @[inline]
                                                                                                                                                                                                                                                                                                                                          def Aesop.Goal.setSuccessProbability (successProbability : Percent) (g : Goal) :
                                                                                                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                                                                                                                                                              @[inline]
                                                                                                                                                                                                                                                                                                                                              def Aesop.Goal.setAddedInIteration (addedInIteration : Iteration) (g : Goal) :
                                                                                                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                                                                                                                                                  @[inline]
                                                                                                                                                                                                                                                                                                                                                  def Aesop.Goal.setLastExpandedInIteration (lastExpandedInIteration : Iteration) (g : Goal) :
                                                                                                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                                                                                                                                                      @[inline]
                                                                                                                                                                                                                                                                                                                                                      def Aesop.Goal.setUnsafeRulesSelected (unsafeRulesSelected : Bool) (g : Goal) :
                                                                                                                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                                                                                                                                                                          @[inline]
                                                                                                                                                                                                                                                                                                                                                          def Aesop.Goal.setUnsafeQueue (unsafeQueue : UnsafeQueue) (g : Goal) :
                                                                                                                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                                                                                                                                                                              @[inline]
                                                                                                                                                                                                                                                                                                                                                              def Aesop.Goal.setState (state : GoalState) (g : Goal) :
                                                                                                                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                                                                                                                                                                  @[inline]
                                                                                                                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                                                                                                                                        @[inline]
                                                                                                                                                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                                                                                                                                                          Instances For
                                                                                                                                                                                                                                                                                                                                                                            @[inline]
                                                                                                                                                                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                                                                                                                                                                              Instances For
                                                                                                                                                                                                                                                                                                                                                                                @[inline]
                                                                                                                                                                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                                                                                                                                                                                                    @[inline]
                                                                                                                                                                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                                                                                                                                                                      Instances For
                                                                                                                                                                                                                                                                                                                                                                                        @[inline]
                                                                                                                                                                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                                                                                                                                                                          Instances For
                                                                                                                                                                                                                                                                                                                                                                                            @[inline]
                                                                                                                                                                                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                                                                                                                                                                                              Instances For
                                                                                                                                                                                                                                                                                                                                                                                                @[inline]
                                                                                                                                                                                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                                                                                                                                                                                                                    @[inline]
                                                                                                                                                                                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                                                                                                                                                                                      Instances For
                                                                                                                                                                                                                                                                                                                                                                                                        @[inline]
                                                                                                                                                                                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                                                                                                                                                                                          Instances For
                                                                                                                                                                                                                                                                                                                                                                                                            @[inline]
                                                                                                                                                                                                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                                                                                                                                                                                                              Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                @[inline]
                                                                                                                                                                                                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                    @[inline]
                                                                                                                                                                                                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                                                                                                                                                                                                      Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                        @[inline]
                                                                                                                                                                                                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                                                                                                                                                                                                          Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                            @[inline]
                                                                                                                                                                                                                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                                                                                                                                                                                                                              Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                @[inline]
                                                                                                                                                                                                                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                    @[inline]
                                                                                                                                                                                                                                                                                                                                                                                                                                    def Aesop.Rapp.setId (id : RappId) (r : Rapp) :
                                                                                                                                                                                                                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                      Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                        @[inline]
                                                                                                                                                                                                                                                                                                                                                                                                                                        def Aesop.Rapp.setParent (parent : GoalRef) (r : Rapp) :
                                                                                                                                                                                                                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                          Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                            @[inline]
                                                                                                                                                                                                                                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                              Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                                @[inline]
                                                                                                                                                                                                                                                                                                                                                                                                                                                def Aesop.Rapp.setState (state : NodeState) (r : Rapp) :
                                                                                                                                                                                                                                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                                    @[inline]
                                                                                                                                                                                                                                                                                                                                                                                                                                                    def Aesop.Rapp.setIsIrrelevant (isIrrelevant : Bool) (r : Rapp) :
                                                                                                                                                                                                                                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                      Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                                        @[inline]
                                                                                                                                                                                                                                                                                                                                                                                                                                                        def Aesop.Rapp.setAppliedRule (appliedRule : RegularRule) (r : Rapp) :
                                                                                                                                                                                                                                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                          Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                                            @[inline]
                                                                                                                                                                                                                                                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                              Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                                                @[inline]
                                                                                                                                                                                                                                                                                                                                                                                                                                                                def Aesop.Rapp.setOriginalSubgoals (originalSubgoals : Array Lean.MVarId) (r : Rapp) :
                                                                                                                                                                                                                                                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                                                    @[inline]
                                                                                                                                                                                                                                                                                                                                                                                                                                                                    def Aesop.Rapp.setSuccessProbability (successProbability : Percent) (r : Rapp) :
                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                      Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                                                        @[inline]
                                                                                                                                                                                                                                                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                          Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                                                            @[inline]
                                                                                                                                                                                                                                                                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                              Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                @[inline]
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Equations

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      Miscellaneous Queries #

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              def Aesop.Rapp.foldSubgoalsM {m : TypeType} {σ : Type} [Monad m] [MonadLiftT (ST IO.RealWorld) m] (init : σ) (f : σGoalRefm σ) (r : Rapp) :
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              m σ
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  def Aesop.Rapp.forSubgoalsM {m : TypeType} [Monad m] [MonadLiftT (ST IO.RealWorld) m] (f : GoalRefm Unit) (r : Rapp) :
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            Instances For