structure Aesop.Frontend.ElabOptions : Type

• parsePriorities : Bool
• parseBuilderOptions : Bool

def Aesop.Frontend.ElabOptions.forAdditionalRules : Aesop.Frontend.ElabOptions

Equations

• Aesop.Frontend.ElabOptions.forAdditionalRules = { parsePriorities := true, parseBuilderOptions := true }

def Aesop.Frontend.ElabOptions.forErasing : Aesop.Frontend.ElabOptions

Equations

• Aesop.Frontend.ElabOptions.forErasing = { parsePriorities := false, parseBuilderOptions := false }

@[inline, reducible]

abbrev Aesop.Frontend.ElabM (α : Type) : Type

Equations

• Aesop.Frontend.ElabM = ReaderT Aesop.Frontend.ElabOptions Lean.Elab.TermElabM

instance Aesop.Frontend.instMonadElabM : Monad Aesop.Frontend.ElabM

Equations

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