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

- opts.applyTransparency = opts.transparency?.getD Lean.Meta.TransparencyMode.default

Instances For

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

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

Instances For

source
def Aesop.RuleBuilder.getApplyIndexingMode (indexMd : Lean.Meta.TransparencyMode) (type : Lean.Expr) :
Lean.MetaM IndexingMode
Equations

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

Instances For

source
def Aesop.RuleBuilder.checkNoIff (type : Lean.Expr) :
Lean.MetaM Unit
Equations

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

Instances For

source
def Aesop.RuleBuilder.applyCore (t : ElabRuleTerm) (pat? : Option RulePattern) (imode? : Option IndexingMode) (md indexMd : Lean.Meta.TransparencyMode) (phase : PhaseSpec) :
Lean.MetaM LocalRuleSetMember
Equations

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

Instances For

source
def Aesop.RuleBuilder.apply :
RuleBuilder
Equations

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

Instances For