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
• lctxInitIndices : Nat
• 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'
• statsRef : Aesop.StatsRef

instance Aesop.SearchM.instNonemptyContext : Nonempty Aesop.SearchM.Context

Equations

• Aesop.SearchM.instNonemptyContext = ⋯

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 } }

@[reducible, inline]

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

Equations

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

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

Equations

• Aesop.SearchM.instMonad = let __src := inferInstanceAs (Monad (Aesop.SearchM Q)); Monad.mk

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

Equations

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

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

Equations

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

instance Aesop.SearchM.instMonadStateState {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.instMonadReaderContext {Q : Type} [Aesop.Queue Q] : MonadReader Aesop.SearchM.Context (Aesop.SearchM Q)

Equations

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

instance Aesop.SearchM.instMonadStats {Q : Type} [Aesop.Queue Q] : Aesop.MonadStats (Aesop.SearchM Q)

Equations

• Aesop.SearchM.instMonadStats = Aesop.MonadStats.mk do let __do_lift ← read pure __do_lift.statsRef

instance Aesop.SearchM.instMonadLiftTreeM {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} (ctx : Aesop.SearchM.Context) (σ : Aesop.SearchM.State Q) (t : Aesop.Tree) (x : Aesop.SearchM Q α) : Lean.MetaM (α × Aesop.SearchM.State Q × Aesop.Tree × Aesop.Stats)

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) (stats : Aesop.Stats) (x : Aesop.SearchM Q α) : Lean.MetaM (α × Aesop.SearchM.State Q × Aesop.Tree × Aesop.Stats)

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