structure Aesop.ForwardBuilderOptionsextends Aesop.RegularBuilderOptions : Type

• indexingMode? : Option Aesop.IndexingMode
• immediateHyps : Option (Array Lean.Name)
• clear : Bool
• 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.instInhabitedForwardBuilderOptions : Inhabited Aesop.ForwardBuilderOptions

Equations

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

def Aesop.ForwardBuilderOptions.default (clear : Bool) : Aesop.ForwardBuilderOptions

Equations

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

def Aesop.RuleBuilder.getImmediatePremises (name : Lean.Name) (type : Lean.Expr) (md : Lean.Meta.TransparencyMode) : Option (Array Lean.Name) → Lean.MetaM (Aesop.UnorderedArraySet Nat)

Equations

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

def Aesop.RuleBuilder.forward (opts : Aesop.ForwardBuilderOptions) : Aesop.RuleBuilder

Equations

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

def Aesop.RuleBuilder.forward.mkResult (opts : Aesop.ForwardBuilderOptions) (tac : Aesop.RuleTacDescr) (type : Lean.Expr) (immediate : Aesop.UnorderedArraySet Nat) : Lean.MetaM Aesop.RuleBuilderResult

Equations

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