structure Aesop.Options'extends Aesop.Options : Type

• strategy : Aesop.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

Instances For

• Aesop.instInhabitedOptions'

instance Aesop.instInhabitedOptions' : Inhabited Aesop.Options'

Equations

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

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

Equations

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