structure Aesop.ElabM.Context : Type

• parsePriorities : Bool
• goal : Lean.MVarId

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

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

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

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

@[reducible, inline]

abbrev Aesop.ElabM (α : Type) : Type

instance Aesop.instMonadElabM : Monad ElabM

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

def Aesop.shouldParsePriorities : ElabM Bool

def Aesop.getGoal : ElabM Lean.MVarId