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

Equations

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

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

Equations

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

def Aesop.RuleBuilder.apply : Aesop.RuleBuilder

Equations

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

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

Equations

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