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

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

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

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

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

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

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

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

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

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

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.

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

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

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 := { }) (simpConfig : Lean.Meta.Simp.Config := { }) (simpConfigSyntax? : Option Lean.Term := none) (stats : Stats := ∅) : Lean.MetaM (Array Lean.MVarId × Stats)