structure Aesop.Options'extends Aesop.Options : Type

• strategy : Strategy
• maxRuleApplicationDepth : Nat
• maxRuleApplications : Nat
• maxGoals : Nat
• maxNormIterations : Nat
• maxSafePrefixRuleApplications : Nat
• maxRuleHeartbeats : Nat
• maxSimpHeartbeats : Nat
• maxUnfoldHeartbeats : Nat
• applyHypsTransparency : Lean.Meta.TransparencyMode
• assumptionTransparency : Lean.Meta.TransparencyMode
• destructProductsTransparency : Lean.Meta.TransparencyMode
• introsTransparency? : Option Lean.Meta.TransparencyMode
• terminal : Bool
• warnOnNonterminal : Bool
• traceScript : Bool
• enableSimp : Bool
• useSimpAll : Bool
• useDefaultSimpSet : Bool
• enableUnfold : Bool
• generateScript : Bool
• forwardMaxDepth? : Option Nat

instance Aesop.instInhabitedOptions' : Inhabited Options'

Equations

• Aesop.instInhabitedOptions' = { default := Aesop.instInhabitedOptions'.default }

def Aesop.instInhabitedOptions'.default : Options'

Equations

• Aesop.instInhabitedOptions'.default = { toOptions := default, generateScript := default, forwardMaxDepth? := default }

def Aesop.Options.toOptions' {m : Type → Type} [Monad m] [Lean.MonadOptions m] (opts : Options) (forwardMaxDepth? : Option Nat := none) : m Options'

Equations

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