def Aesop.CasesPattern.check (decl : Lean.Name) (p : Aesop.CasesPattern) : Lean.MetaM Unit

Equations

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

def Aesop.CasesPattern.toIndexingMode (p : Aesop.CasesPattern) : Lean.MetaM Aesop.IndexingMode

Equations

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

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

Equations

• Aesop.RuleBuilderOptions.casesTransparency opts = Option.getD opts.transparency? Lean.Meta.TransparencyMode.reducible

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

Equations

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

def Aesop.RuleBuilderOptions.casesPatterns (opts : Aesop.RuleBuilderOptions) : Array Aesop.CasesPattern

Equations

• Aesop.RuleBuilderOptions.casesPatterns opts = Option.getD opts.casesPatterns? #[]

def Aesop.RuleBuilderOptions.casesIndexingMode (decl : Lean.Name) (opts : Aesop.RuleBuilderOptions) : Lean.MetaM Aesop.IndexingMode

Equations

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

def Aesop.RuleBuilderOptions.casesTarget (decl : Lean.Name) (opts : Aesop.RuleBuilderOptions) : Aesop.CasesTarget

Equations

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

def Aesop.RuleBuilder.cases : Aesop.RuleBuilder

Equations

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