structure Aesop.ApplyBuilderOptionsextends Aesop.RegularBuilderOptions : Type

• indexingMode? : Option Aesop.IndexingMode
• transparency : Lean.Meta.TransparencyMode

  The transparency used by the rule tactic.

• indexTransparency : Lean.Meta.TransparencyMode

  The transparency used to index the rule. The rule is not indexed unless this is .reducible.

instance Aesop.instInhabitedApplyBuilderOptions : Inhabited Aesop.ApplyBuilderOptions

Equations

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

def Aesop.RuleBuilder.apply (opts : Aesop.ApplyBuilderOptions) : Aesop.RuleBuilder

Equations

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

def Aesop.RuleBuilder.apply.mkResult (opts : Aesop.ApplyBuilderOptions) (tac : Aesop.RuleTacDescr) (type : Lean.Expr) : Lean.MetaM Aesop.RuleBuilderResult

Equations

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