Documentation

Aesop.Search.Main

Equations
    Instances For
      def Aesop.expandNextGoal.fmt {Q : Type} [Queue Q] (id : GoalId) (priority : Percent) (initialGoal : Lean.MVarId) (initialMetaState : Lean.Meta.SavedState) (result : Except Lean.Exception RuleResult) :
      Equations
        Instances For
          Equations
            Instances For
              Equations
                Instances For
                  Equations
                    Instances For
                      Equations
                        Instances For
                          Equations
                            Instances For
                              Equations
                                Instances For
                                  def Aesop.traceScript {Q : Type} [Queue Q] (completeProof : Bool) :
                                  Equations
                                    Instances For
                                      Equations
                                        Instances For
                                          Equations
                                            Instances For

                                              This function detects whether the search has made progress, meaning that the remaining goals after safe prefix expansion are different from the initial goal. We approximate this by checking whether, after safe prefix expansion, either of the following statements is true.

                                              • There is a safe rapp.
                                              • A subgoal of the preprocessing rule has been modified during normalisation.

                                              This is an approximation because a safe rule could, in principle, leave the initial goal unchanged.

                                              Equations
                                                Instances For
                                                  def Aesop.throwAesopEx {Q : Type} [Queue Q] {α : Type} (mvarId : Lean.MVarId) (remainingSafeGoals : Array Lean.MVarId) (safePrefixExpansionSuccess : Bool) (msg? : Option Lean.MessageData) :
                                                  SearchM Q α
                                                  Equations
                                                    Instances For
                                                      Equations
                                                        Instances For
                                                          def Aesop.search (goal : Lean.MVarId) (ruleSet? : Option LocalRuleSet := none) (options : Options := { }) (simpConfig : Lean.Meta.Simp.Config := { }) (simpConfigSyntax? : Option Lean.Term := none) (stats : Stats := ) :
                                                          Equations
                                                            Instances For