structure Aesop.NormSimpContextextends Lean.Meta.Simp.Context : Type

• config : Lean.Meta.Simp.Config
• maxDischargeDepth : UInt32
• simpTheorems : Lean.Meta.SimpTheoremsArray
• congrTheorems : Lean.Meta.SimpCongrTheorems
• parent? : Option Lean.Expr
• dischargeDepth : UInt32
• enabled : Bool
• useHyps : Bool
• configStx? : Option Lean.Term
• simprocs : Lean.Meta.Simp.SimprocsArray

instance Aesop.instInhabitedNormSimpContext : Inhabited Aesop.NormSimpContext

Equations

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

structure Aesop.SearchM.Context : Type

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

instance Aesop.SearchM.instInhabitedContext : Inhabited Aesop.SearchM.Context

Equations

• Aesop.SearchM.instInhabitedContext = { default := { ruleSet := default, normSimpContext := default, options := default } }

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

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

instance Aesop.SearchM.instInhabitedState : {a : Type} → [inst : Inhabited a] → {a_1 : Aesop.Queue a} → Inhabited (Aesop.SearchM.State a)

Equations

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

@[inline, reducible]

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

Equations

• Aesop.SearchBaseM Q = ReaderT Aesop.SearchM.Context (StateRefT' IO.RealWorld (Aesop.SearchM.State Q) (StateRefT' IO.RealWorld Aesop.Tree Lean.MetaM))

@[inline, reducible]

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

Equations

• Aesop.SearchM Q = Aesop.ProfileT (Aesop.SearchBaseM Q)

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

Equations

• Aesop.SearchM.instMonadSearchM = let src := inferInstanceAs (Monad (Aesop.SearchM Q)); Monad.mk

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

Equations

• Aesop.SearchM.instMonadRefSearchM = let src := inferInstanceAs (Lean.MonadRef (Aesop.SearchM Q)); { getRef := Lean.getRef, withRef := fun {α : Type} => Lean.MonadRef.withRef }

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

Equations

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

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

Equations

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

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

Equations

• Aesop.SearchM.instMonadReaderContextSearchM = let src := inferInstanceAs (MonadReaderOf Aesop.SearchM.Context (Aesop.SearchM Q)); { read := MonadReaderOf.read }

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

Equations

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

def Aesop.SearchM.run' {Q : Type} [Aesop.Queue Q] {α : Type} (profile : Aesop.Profile) (ctx : Aesop.SearchM.Context) (σ : Aesop.SearchM.State Q) (t : Aesop.Tree) (x : Aesop.SearchM Q α) : Lean.MetaM (α × Aesop.SearchM.State Q × Aesop.Tree × Aesop.Profile)

Equations

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

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

Equations

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

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

Equations

• Aesop.getTree = getThe Aesop.Tree

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

Equations

• Aesop.setTree = Aesop.setThe Aesop.Tree

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

Equations

• Aesop.modifyTree = modifyThe Aesop.Tree

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

def Aesop.setMaxRuleApplicationDepthReached {Q : Type} [Aesop.Queue Q] : Aesop.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} [Aesop.Queue Q] : Aesop.SearchM Q Bool

Equations

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