structure Aesop.ElabM.Context : Type

• parsePriorities : Bool
• goal : Lean.MVarId

def Aesop.ElabM.Context.forAdditionalRules (goal : Lean.MVarId) : Aesop.ElabM.Context

Equations

• Aesop.ElabM.Context.forAdditionalRules goal = { parsePriorities := true, goal := goal }

def Aesop.ElabM.Context.forAdditionalGlobalRules : Lean.MetaM Aesop.ElabM.Context

Equations

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

def Aesop.ElabM.Context.forErasing (goal : Lean.MVarId) : Aesop.ElabM.Context

Equations

• Aesop.ElabM.Context.forErasing goal = { parsePriorities := false, goal := goal }

def Aesop.ElabM.Context.forGlobalErasing : Lean.MetaM Aesop.ElabM.Context

Equations

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

@[inline, reducible]

abbrev Aesop.ElabM (α : Type) : Type

Equations

• Aesop.ElabM = ReaderT Aesop.ElabM.Context Lean.Elab.TermElabM

instance Aesop.instMonadElabM : Monad Aesop.ElabM

Equations

• Aesop.instMonadElabM = let __src := inferInstanceAs (Monad Aesop.ElabM); Monad.mk

def Aesop.ElabM.run {α : Type} (ctx : Aesop.ElabM.Context) (x : Aesop.ElabM α) : Lean.Elab.TermElabM α

Equations

• Aesop.ElabM.run ctx x = ReaderT.run x ctx

def Aesop.shouldParsePriorities : Aesop.ElabM Bool

Equations

• Aesop.shouldParsePriorities = do let __do_lift ← read pure __do_lift.parsePriorities

def Aesop.getGoal : Aesop.ElabM Lean.MVarId

Equations

• Aesop.getGoal = do let __do_lift ← read pure __do_lift.goal

def Aesop.getRuleName : Lean.Expr → Lean.MetaM Lean.Name

Equations

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