Documentation

Aesop.Tree.Data

Node IDs #

structure Aesop.GoalId :
Instances For
    def Aesop.instDecidableEqGoalId.decEq (x✝ x✝¹ : GoalId) :
    Decidable (x✝ = x✝¹)
    Equations
    Instances For
      Equations
      Instances For
        Equations
        Instances For
          Equations
          Instances For
            Equations
            Instances For
              Equations

              Rule Application IDs #

              structure Aesop.RappId :
              Instances For
                def Aesop.instDecidableEqRappId.decEq (x✝ x✝¹ : RappId) :
                Decidable (x✝ = x✝¹)
                Equations
                Instances For
                  Equations
                  Instances For
                    Equations
                    Instances For
                      Equations
                      Instances For
                        Equations
                        Instances For
                          Equations

                          Iterations #

                          Equations
                          Instances For

                            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
                              • One or more equations did not get rendered due to their size.

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

                              Instances For
                                Equations
                                • One or more equations did not get rendered due to their size.

                                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
                                        Equations
                                        Instances For
                                          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
                                              • One or more equations did not get rendered due to their size.
                                              Instances For
                                                @[implemented_by Aesop.treeImpl]
                                                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
                                                            • One or more equations did not get rendered due to their size.
                                                            Instances For
                                                              @[inline]
                                                              Equations
                                                              Instances For
                                                                @[inline]
                                                                Equations
                                                                • One or more equations did not get rendered due to their size.
                                                                Instances For
                                                                  @[inline]
                                                                  Equations
                                                                  • One or more equations did not get rendered due to their size.
                                                                  Instances For
                                                                    @[inline]
                                                                    Equations
                                                                    Instances For
                                                                      @[inline]
                                                                      Equations
                                                                      • One or more equations did not get rendered due to their size.
                                                                      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
                                                                                                • One or more equations did not get rendered due to their size.
                                                                                                Instances For
                                                                                                  @[inline]
                                                                                                  Equations
                                                                                                  • One or more equations did not get rendered due to their size.
                                                                                                  Instances For
                                                                                                    @[inline]
                                                                                                    def Aesop.Goal.setChildren (children : Array RappRef) (g : Goal) :
                                                                                                    Equations
                                                                                                    • One or more equations did not get rendered due to their size.
                                                                                                    Instances For
                                                                                                      @[inline]
                                                                                                      Equations
                                                                                                      • One or more equations did not get rendered due to their size.
                                                                                                      Instances For
                                                                                                        @[inline]
                                                                                                        def Aesop.Goal.setDepth (depth : Nat) (g : Goal) :
                                                                                                        Equations
                                                                                                        • One or more equations did not get rendered due to their size.
                                                                                                        Instances For
                                                                                                          @[inline]
                                                                                                          def Aesop.Goal.setIsIrrelevant (isIrrelevant : Bool) (g : Goal) :
                                                                                                          Equations
                                                                                                          • One or more equations did not get rendered due to their size.
                                                                                                          Instances For
                                                                                                            @[inline]
                                                                                                            def Aesop.Goal.setIsForcedUnprovable (isForcedUnprovable : Bool) (g : Goal) :
                                                                                                            Equations
                                                                                                            • One or more equations did not get rendered due to their size.
                                                                                                            Instances For
                                                                                                              @[inline]
                                                                                                              def Aesop.Goal.setPreNormGoal (preNormGoal : Lean.MVarId) (g : Goal) :
                                                                                                              Equations
                                                                                                              • One or more equations did not get rendered due to their size.
                                                                                                              Instances For
                                                                                                                @[inline]
                                                                                                                Equations
                                                                                                                • One or more equations did not get rendered due to their size.
                                                                                                                Instances For
                                                                                                                  @[inline]
                                                                                                                  Equations
                                                                                                                  • One or more equations did not get rendered due to their size.
                                                                                                                  Instances For
                                                                                                                    @[inline]
                                                                                                                    def Aesop.Goal.setForwardState (forwardState : ForwardState) (g : Goal) :
                                                                                                                    Equations
                                                                                                                    • One or more equations did not get rendered due to their size.
                                                                                                                    Instances For
                                                                                                                      @[inline]
                                                                                                                      Equations
                                                                                                                      • One or more equations did not get rendered due to their size.
                                                                                                                      Instances For
                                                                                                                        @[inline]
                                                                                                                        def Aesop.Goal.setSuccessProbability (successProbability : Percent) (g : Goal) :
                                                                                                                        Equations
                                                                                                                        • One or more equations did not get rendered due to their size.
                                                                                                                        Instances For
                                                                                                                          @[inline]
                                                                                                                          def Aesop.Goal.setAddedInIteration (addedInIteration : Iteration) (g : Goal) :
                                                                                                                          Equations
                                                                                                                          • One or more equations did not get rendered due to their size.
                                                                                                                          Instances For
                                                                                                                            @[inline]
                                                                                                                            def Aesop.Goal.setLastExpandedInIteration (lastExpandedInIteration : Iteration) (g : Goal) :
                                                                                                                            Equations
                                                                                                                            • One or more equations did not get rendered due to their size.
                                                                                                                            Instances For
                                                                                                                              @[inline]
                                                                                                                              def Aesop.Goal.setUnsafeRulesSelected (unsafeRulesSelected : Bool) (g : Goal) :
                                                                                                                              Equations
                                                                                                                              • One or more equations did not get rendered due to their size.
                                                                                                                              Instances For
                                                                                                                                @[inline]
                                                                                                                                def Aesop.Goal.setUnsafeQueue (unsafeQueue : UnsafeQueue) (g : Goal) :
                                                                                                                                Equations
                                                                                                                                • One or more equations did not get rendered due to their size.
                                                                                                                                Instances For
                                                                                                                                  @[inline]
                                                                                                                                  def Aesop.Goal.setState (state : GoalState) (g : Goal) :
                                                                                                                                  Equations
                                                                                                                                  • One or more equations did not get rendered due to their size.
                                                                                                                                  Instances For
                                                                                                                                    @[inline]
                                                                                                                                    Equations
                                                                                                                                    • One or more equations did not get rendered due to their size.
                                                                                                                                    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]
                                                                                                                                                    def Aesop.Rapp.setId (id : RappId) (r : Rapp) :
                                                                                                                                                    Equations
                                                                                                                                                    • One or more equations did not get rendered due to their size.
                                                                                                                                                    Instances For
                                                                                                                                                      @[inline]
                                                                                                                                                      def Aesop.Rapp.setParent (parent : GoalRef) (r : Rapp) :
                                                                                                                                                      Equations
                                                                                                                                                      • One or more equations did not get rendered due to their size.
                                                                                                                                                      Instances For
                                                                                                                                                        @[inline]
                                                                                                                                                        Equations
                                                                                                                                                        • One or more equations did not get rendered due to their size.
                                                                                                                                                        Instances For
                                                                                                                                                          @[inline]
                                                                                                                                                          def Aesop.Rapp.setState (state : NodeState) (r : Rapp) :
                                                                                                                                                          Equations
                                                                                                                                                          • One or more equations did not get rendered due to their size.
                                                                                                                                                          Instances For
                                                                                                                                                            @[inline]
                                                                                                                                                            def Aesop.Rapp.setIsIrrelevant (isIrrelevant : Bool) (r : Rapp) :
                                                                                                                                                            Equations
                                                                                                                                                            • One or more equations did not get rendered due to their size.
                                                                                                                                                            Instances For
                                                                                                                                                              @[inline]
                                                                                                                                                              def Aesop.Rapp.setAppliedRule (appliedRule : RegularRule) (r : Rapp) :
                                                                                                                                                              Equations
                                                                                                                                                              • One or more equations did not get rendered due to their size.
                                                                                                                                                              Instances For
                                                                                                                                                                @[inline]
                                                                                                                                                                Equations
                                                                                                                                                                • One or more equations did not get rendered due to their size.
                                                                                                                                                                Instances For
                                                                                                                                                                  @[inline]
                                                                                                                                                                  def Aesop.Rapp.setOriginalSubgoals (originalSubgoals : Array Lean.MVarId) (r : Rapp) :
                                                                                                                                                                  Equations
                                                                                                                                                                  • One or more equations did not get rendered due to their size.
                                                                                                                                                                  Instances For
                                                                                                                                                                    @[inline]
                                                                                                                                                                    def Aesop.Rapp.setSuccessProbability (successProbability : Percent) (r : Rapp) :
                                                                                                                                                                    Equations
                                                                                                                                                                    • One or more equations did not get rendered due to their size.
                                                                                                                                                                    Instances For
                                                                                                                                                                      @[inline]
                                                                                                                                                                      Equations
                                                                                                                                                                      • One or more equations did not get rendered due to their size.
                                                                                                                                                                      Instances For
                                                                                                                                                                        @[inline]
                                                                                                                                                                        Equations
                                                                                                                                                                        • One or more equations did not get rendered due to their size.
                                                                                                                                                                        Instances For
                                                                                                                                                                          @[inline]
                                                                                                                                                                          Equations
                                                                                                                                                                          • One or more equations did not get rendered due to their size.
                                                                                                                                                                          Instances For
                                                                                                                                                                            Equations

                                                                                                                                                                            Miscellaneous Queries #

                                                                                                                                                                            @[inline]
                                                                                                                                                                            Equations
                                                                                                                                                                            Instances For
                                                                                                                                                                              Equations
                                                                                                                                                                              Instances For
                                                                                                                                                                                Equations
                                                                                                                                                                                • One or more equations did not get rendered due to their size.
                                                                                                                                                                                Instances For
                                                                                                                                                                                  Equations
                                                                                                                                                                                  • One or more equations did not get rendered due to their size.
                                                                                                                                                                                  Instances For
                                                                                                                                                                                    Equations
                                                                                                                                                                                    Instances For
                                                                                                                                                                                      Equations
                                                                                                                                                                                      Instances For
                                                                                                                                                                                        Equations
                                                                                                                                                                                        Instances For
                                                                                                                                                                                          Equations
                                                                                                                                                                                          Instances For
                                                                                                                                                                                            Equations
                                                                                                                                                                                            • One or more equations did not get rendered due to their size.
                                                                                                                                                                                            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
                                                                                                                                                                                                    • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                    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
                                                                                                                                                                                                            Equations
                                                                                                                                                                                                            Instances For

                                                                                                                                                                                                              Get a DeclNameGenerator for auxiliary declarations that can be used by children of this rapp. Successive calls to this function return DeclNameGenerators that are guaranteed to generate distinct names.

                                                                                                                                                                                                              Equations
                                                                                                                                                                                                              • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                              Instances For