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

Equations

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

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

Equations

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

def Aesop.RuleBuilder.getConstructorsIndexingMode (indexMd : Lean.Meta.TransparencyMode) (info : Lean.InductiveVal) : Lean.MetaM IndexingMode

Equations

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

def Aesop.RuleBuilder.constructorsCore (info : Lean.InductiveVal) (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.

def Aesop.RuleBuilder.constructors : RuleBuilder

Equations

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