structure Aesop.NormSimpContext : Type

• toContext : Lean.Meta.Simp.Context
• enabled : Bool
• useHyps : Bool
• configStx? : Option Lean.Term
• simprocs : Lean.Meta.Simp.SimprocsArray

instance Aesop.instInhabitedNormSimpContext : Inhabited NormSimpContext

structure Aesop.SearchM.Context : Type

• ruleSet : LocalRuleSet
• normSimpContext : NormSimpContext
• options : Options'

instance Aesop.SearchM.instNonemptyContext : Nonempty Context

structure Aesop.SearchM.State (Q : Type) [Queue Q] : Type

• iteration : Iteration
• queue : Q
• maxRuleApplicationDepthReached : Bool

instance Aesop.SearchM.instInhabitedState {a✝ : Type} [Inhabited a✝] {a✝¹ : Queue a✝} : Inhabited (State a✝)

@[reducible, inline]

abbrev Aesop.SearchM (Q : Type) [Queue Q] (α : Type) : Type

instance Aesop.SearchM.instMonad {Q : Type} [Queue Q] : Monad (SearchM Q)

instance Aesop.SearchM.instMonadRef {Q : Type} [Queue Q] : Lean.MonadRef (SearchM Q)

instance Aesop.SearchM.instInhabited {Q : Type} [Queue Q] {α : Type} : Inhabited (SearchM Q α)

instance Aesop.SearchM.instMonadStateState {Q : Type} [Queue Q] : MonadState (State Q) (SearchM Q)

instance Aesop.SearchM.instMonadReaderContext {Q : Type} [Queue Q] : MonadReader Context (SearchM Q)

instance Aesop.SearchM.instMonadLiftTreeM {Q : Type} [Queue Q] : MonadLift TreeM (SearchM Q)

def Aesop.SearchM.run' {Q : Type} [Queue Q] {α : Type} (ctx : Context) (σ : State Q) (tree : Tree) (x : SearchM Q α) : BaseM (α × State Q × Tree)

def Aesop.SearchM.run {Q : Type} [Queue Q] {α : Type} (ruleSet : LocalRuleSet) (options : Options') (simpConfig : Lean.Meta.Simp.Config) (simpConfigStx? : Option Lean.Term) (goal : Lean.MVarId) (x : SearchM Q α) : BaseM (α × State Q × Tree)

def Aesop.getTree {Q : Type} [Queue Q] : SearchM Q Tree

def Aesop.setTree {Q : Type} [Queue Q] : Tree → SearchM Q Unit

def Aesop.modifyTree {Q : Type} [Queue Q] : (Tree → Tree) → SearchM Q Unit

def Aesop.getIteration {Q : Type} [Queue Q] : SearchM Q Iteration

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

def Aesop.popGoal? {Q : Type} [Queue Q] : SearchM Q (Option GoalRef)

def Aesop.enqueueGoals {Q : Type} [Queue Q] (gs : Array GoalRef) : SearchM Q Unit

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

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