partial def Aesop.nextActiveGoal {Q : Type} [Queue Q] : SearchM Q GoalRef

def Aesop.expandNextGoal {Q : Type} [Queue Q] : SearchM Q Unit

Equations

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

def Aesop.expandNextGoal.fmt {Q : Type} [Queue Q] (id : GoalId) (priority : Percent) (initialGoal : Lean.MVarId) (initialMetaState : Lean.Meta.SavedState) (result : Except Lean.Exception RuleResult) : SearchM Q Lean.MessageData

Equations

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

def Aesop.expandNextGoal.traceNewRapps {Q : Type} [Queue Q] (newRapps : Array RappRef) : SearchM Q Unit

Equations

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

def Aesop.checkGoalLimit {Q : Type} [Queue Q] : SearchM Q (Option Lean.MessageData)

Equations

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

def Aesop.checkRappLimit {Q : Type} [Queue Q] : SearchM Q (Option Lean.MessageData)

Equations

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

def Aesop.checkRootUnprovable {Q : Type} [Queue Q] : SearchM Q (Option Lean.MessageData)

Equations

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

def Aesop.getProof? {Q : Type} [Queue Q] : SearchM Q (Option Lean.Expr)

Equations

• Aesop.getProof? = do let __do_lift ← liftM Aesop.getRootMVarId Lean.getExprMVarAssignment? __do_lift

def Aesop.finalizeProof {Q : Type} [Queue Q] : SearchM Q Unit

Equations

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

def Aesop.traceScript {Q : Type} [Queue Q] (completeProof : Bool) : SearchM Q Unit

Equations

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

def Aesop.traceTree {Q : Type} [Queue Q] : SearchM Q Unit

Equations

• Aesop.traceTree = do let __do_lift ← liftM Aesop.getRootGoal let __do_lift ← ST.Ref.get __do_lift liftM (__do_lift.traceTree Aesop.TraceOption.tree)

def Aesop.finishIfProven {Q : Type} [Queue Q] : SearchM Q Bool

Equations

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

def Aesop.treeHasProgress : TreeM Bool

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.

def Aesop.throwAesopEx {Q : Type} [Queue Q] {α : Type} (mvarId : Lean.MVarId) (remainingSafeGoals : Array Lean.MVarId) (safePrefixExpansionSuccess : Bool) (msg? : Option Lean.MessageData) : SearchM Q α

Equations

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

def Aesop.handleNonfatalError {Q : Type} [Queue Q] (err : Lean.MessageData) : SearchM Q (Array Lean.MVarId)

Equations

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

partial def Aesop.searchLoop {Q : Type} [Queue Q] : SearchM Q (Array Lean.MVarId)

def Aesop.search (goal : Lean.MVarId) (ruleSet? : Option LocalRuleSet := none) (options : Options := { strategy := 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 : 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 := true, zetaUnused := true }) (simpConfigSyntax? : Option Lean.Term := none) (stats : Stats := ∅) : Lean.MetaM (Array Lean.MVarId × Stats)

Equations

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