structure Aesop.NormSimpContext : Type

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

def Aesop.instInhabitedNormSimpContext.default : NormSimpContext

Equations

• Aesop.instInhabitedNormSimpContext.default = { toContext := default, enabled := default, useHyps := default, configStx? := default, simprocs := default }

@[implicit_reducible]

instance Aesop.instInhabitedNormSimpContext : Inhabited NormSimpContext

Equations

• Aesop.instInhabitedNormSimpContext = { default := Aesop.instInhabitedNormSimpContext.default }

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

@[implicit_reducible]

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

Equations

• Aesop.SearchM.instInhabitedState = { default := Aesop.SearchM.instInhabitedState.default }

def Aesop.SearchM.instInhabitedState.default {a✝ : Type} [Inhabited a✝] {a✝¹ : Queue a✝} : State a✝

Equations

• Aesop.SearchM.instInhabitedState.default = { iteration := default, queue := default, maxRuleApplicationDepthReached := default }

@[reducible, inline]

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

Equations

• Aesop.SearchM Q = ReaderT Aesop.SearchM.Context (StateRefT' IO.RealWorld (Aesop.SearchM.State Q) (StateRefT' IO.RealWorld Aesop.TreeM.State Aesop.BaseM))

@[implicit_reducible]

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

Equations

• Aesop.SearchM.instMonad = inferInstance

@[implicit_reducible]

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

Equations

• Aesop.SearchM.instMonadRef = inferInstance

@[implicit_reducible]

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

Equations

• Aesop.SearchM.instInhabited = { default := failure }

@[implicit_reducible]

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

Equations

• Aesop.SearchM.instMonadStateState = { get := MonadStateOf.get, set := set, modifyGet := @MonadStateOf.modifyGet (Aesop.SearchM.State Q) (Aesop.SearchM Q) inferInstance }

@[implicit_reducible]

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

Equations

• Aesop.SearchM.instMonadReaderContext = { read := MonadReaderOf.read }

@[implicit_reducible]

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

Equations

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

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

Equations

• Aesop.SearchM.run' ctx σ tree x = do let __discr ← ((ReaderT.run x ctx).run σ).run { tree := tree } match __discr with | ((a, σ), t) => pure (a, σ, t.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)

Equations

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

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

Equations

• Aesop.getTree = getThe Aesop.Tree

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

Equations

• Aesop.setTree = Aesop.setThe Aesop.Tree

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

Equations

• Aesop.modifyTree = modifyThe Aesop.Tree

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

Equations

• Aesop.getIteration = do let __do_lift ← get pure __do_lift.iteration

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

• Aesop.setMaxRuleApplicationDepthReached = modify fun (s : Aesop.SearchM.State Q) => { iteration := s.iteration, queue := s.queue, maxRuleApplicationDepthReached := true }

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

Equations

• Aesop.wasMaxRuleApplicationDepthReached = do let __do_lift ← get pure __do_lift.maxRuleApplicationDepthReached