Documentation

Aesop.Search.Main

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
      • 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
          • 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
                • One or more equations did not get rendered due to their size.
                Instances For
                  def Aesop.optimizeScript {Q : Type} [Aesop.Queue Q] (uscript : Aesop.Script.UScript) (rootState : Lean.Meta.SavedState) (rootGoal : Lean.MVarId) :
                  Aesop.SearchM Q (Option (Lean.TSyntax `Lean.Parser.Tactic.tacticSeq))
                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    def Aesop.traceScript {Q : Type} [Aesop.Queue Q] (completeProof : Bool) :
                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      Equations
                      Instances For
                        Equations
                        • One or more equations did not get rendered due to their size.
                        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
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            def Aesop.throwAesopEx {Q : Type} [Aesop.Queue Q] {α : Type} (mvarId : Lean.MVarId) (remainingSafeGoals : Array Lean.MVarId) (safePrefixExpansionSuccess : Bool) (msg? : Option Lean.MessageData) :
                            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
                                def Aesop.search (goal : Lean.MVarId) (ruleSet? : optParam (Option Aesop.LocalRuleSet) none) (options : optParam Aesop.Options { strategy := Aesop.Strategy.bestFirst, maxRuleApplicationDepth := 30, maxRuleApplications := 200, maxGoals := 0, maxNormIterations := 100, maxSafePrefixRuleApplications := 50, maxRuleHeartbeats := 0, maxSimpHeartbeats := 0, maxUnfoldHeartbeats := 0, applyHypsTransparency := Lean.Meta.TransparencyMode.default, assumptionTransparency := Lean.Meta.TransparencyMode.default, destructProductsTransparency := Lean.Meta.TransparencyMode.reducible, introsTransparency? := none, terminal := false, warnOnNonterminal := true, traceScript := false, enableSimp := true, useSimpAll := true, useDefaultSimpSet := true, enableUnfold := true }) (simpConfig : optParam Lean.Meta.Simp.Config { maxSteps := Lean.Meta.Simp.defaultMaxSteps, maxDischargeDepth := 2, contextual := false, memoize := true, singlePass := false, zeta := true, beta := true, eta := true, etaStruct := Lean.Meta.EtaStructMode.all, iota := true, proj := true, decide := false, arith := false, autoUnfold := false, dsimp := true, failIfUnchanged := true, ground := false, unfoldPartialApp := false, zetaDelta := false, index := true, implicitDefEqProofs := false }) (simpConfigSyntax? : optParam (Option Lean.Term) none) (stats : optParam Aesop.Stats ) :
                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For