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

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

instance Aesop.instInhabitedNormSimpContext : Inhabited Aesop.NormSimpContext

Equations

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

structure Aesop.SearchM.Context : Type

• ruleSet : Aesop.RuleSet
• normSimpContext : Aesop.NormSimpContext
• options : Aesop.Options'
• profilingEnabled : Bool

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

Equations

• Aesop.SearchM.instNonemptyContext = Aesop.SearchM.instNonemptyContext.proof_1

def Aesop.SearchM.Context.normSimpConfig (ctx : Aesop.SearchM.Context) : Aesop.SimpConfig

Equations

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

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

• iteration : Aesop.Iteration
• queue : Q
• profile : Aesop.Profile
• 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, profile := default, maxRuleApplicationDepthReached := default } }

@[inline, reducible]

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.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 {α} => 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.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.

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.instMonadReaderOfContextSearchM {Q : Type} [Aesop.Queue Q] : MonadReaderOf Aesop.ProfileT.Context (Aesop.SearchM Q)

Equations

• Aesop.SearchM.instMonadReaderOfContextSearchM = { read := do let __do_lift ← read pure { isProfilingEnabled := __do_lift.profilingEnabled } }

instance Aesop.SearchM.instMonadStateOfProfileSearchM {Q : Type} [Aesop.Queue Q] : MonadStateOf Aesop.Profile (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)

Equations

• Aesop.SearchM.run' ctx σ t x = do let __discr ← StateRefT'.run (StateRefT'.run (ReaderT.run x ctx) σ) t match __discr with | ((a, σ), t) => pure (a, σ, t)

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

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 => { iteration := s.iteration, queue := s.queue, profile := s.profile, 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