source
def Aesop.RuleBuilderOptions.forwardTransparency (opts : RuleBuilderOptions) :
Lean.Meta.TransparencyMode
Equations

- opts.forwardTransparency = opts.transparency?.getD Lean.Meta.TransparencyMode.reducible

Instances For

source
def Aesop.RuleBuilderOptions.forwardIndexTransparency (opts : RuleBuilderOptions) :
Lean.Meta.TransparencyMode
Equations

- opts.forwardIndexTransparency = opts.indexTransparency?.getD Lean.Meta.TransparencyMode.reducible

Instances For

source
def Aesop.RuleBuilder.getForwardIndexingMode (type : Lean.Expr) (immediate : UnorderedArraySet PremiseIndex) :
Lean.MetaM IndexingMode
Equations

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

Instances For

source
def Aesop.RuleBuilder.getImmediatePremises (type : Lean.Expr) (pat? : Option RulePattern) :
Option (Array Lean.Name) → Lean.MetaM (UnorderedArraySet PremiseIndex)
Equations

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

Instances For

source
def Aesop.RuleBuilder.forwardCore₂ (t : ElabRuleTerm) (immediate? : Option (Array Lean.Name)) (pat? : Option RulePattern) (phase : PhaseSpec) (isDestruct : Bool) :
Lean.MetaM ForwardRule
Equations

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

Instances For

source
def Aesop.RuleBuilder.forwardCore (t : ElabRuleTerm) (immediate? : Option (Array Lean.Name)) (pat? : Option RulePattern) (phase : PhaseSpec) (isDestruct : Bool) :
Lean.MetaM LocalRuleSetMember
Equations

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

Instances For

source
def Aesop.RuleBuilder.forward (isDestruct : Bool) :
RuleBuilder
Equations

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

Instances For