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.checkRenderedScript {Q : Type} [Aesop.Queue Q] (completeProof : Bool) (script : Lean.TSyntax `Lean.Parser.Tactic.tacticSeq) :
                  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
                        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