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

Equations

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

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

Equations

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

def Aesop.RuleBuilder.constructors : Aesop.RuleBuilder

Equations

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

def Aesop.RuleBuilder.constructors.name : Aesop.BuilderName

Equations

• Aesop.RuleBuilder.constructors.name = Aesop.BuilderName.constructors

def Aesop.RuleBuilder.constructors.getIndexingMode (opts : Aesop.RuleBuilderOptions) (info : Lean.InductiveVal) : Lean.MetaM Aesop.IndexingMode

Equations

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