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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

def Aesop.checkRenderedScript {Q : Type} [Aesop.Queue Q] (script : Array Lean.Syntax.Tactic) : Aesop.SearchM Q Unit

Equations

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

def Aesop.checkScriptSteps {Q : Type} [Aesop.Queue Q] (script : Aesop.UnstructuredScript) : Aesop.SearchM Q Unit

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

def Aesop.handleFatalError {Q : Type} [Aesop.Queue Q] {α : Type} (e : Lean.Exception) : Aesop.SearchM Q α

Equations

• Aesop.handleFatalError e = do Aesop.traceTree throw e

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

def Aesop.search (goal : Lean.MVarId) (ruleSet? : optParam (Option Aesop.RuleSet) none) (options : optParam Aesop.Options { strategy := Aesop.Strategy.bestFirst, maxRuleApplicationDepth := 30, maxRuleApplications := 200, maxGoals := 0, maxNormIterations := 100, applyHypsTransparency := Lean.Meta.TransparencyMode.default, assumptionTransparency := Lean.Meta.TransparencyMode.default, destructProductsTransparency := Lean.Meta.TransparencyMode.reducible, introsTransparency? := none, terminal := false, warnOnNonterminal := true, traceScript := false }) (simpConfig : optParam Aesop.SimpConfig { toConfigCtx := { toConfig := { maxSteps := Lean.Meta.Simp.defaultMaxSteps, maxDischargeDepth := 1, contextual := true, memoize := true, singlePass := false, zeta := true, beta := true, eta := true, etaStruct := Lean.Meta.EtaStructMode.all, iota := true, proj := true, decide := true, arith := false, autoUnfold := false, dsimp := true, failIfUnchanged := true } }, enabled := true, useHyps := true }) (simpConfigSyntax? : optParam (Option Lean.Term) none) (profile : optParam Aesop.Profile ∅) : Lean.MetaM (Array Lean.MVarId × Aesop.Profile)

Equations

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