structure Aesop.ElabM.Context : Type

• parsePriorities : Bool
• goal : Lean.MVarId

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

@[reducible, inline]

abbrev Aesop.ElabM (α : Type) : Type

Equations

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

instance Aesop.instMonadElabM : Monad ElabM

Equations

• Aesop.instMonadElabM = inferInstanceAs (Monad Aesop.ElabM)

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

Equations

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

def Aesop.shouldParsePriorities : ElabM Bool

Equations

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

def Aesop.getGoal : ElabM Lean.MVarId

Equations

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