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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

def Aesop.RuleBuilder.apply : Aesop.RuleBuilder

Equations

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