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

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

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

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

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

def Aesop.RuleBuilder.mkCasesTarget (decl : Lean.Name) (casesPatterns : Array CasesPattern) : CasesTarget

def Aesop.RuleBuilder.getCasesIndexingMode (decl : Lean.Name) (indexMd : Lean.Meta.TransparencyMode) (casesPatterns : Array CasesPattern) : Lean.MetaM IndexingMode

def Aesop.RuleBuilder.casesCore (decl : Lean.Name) (info : Lean.InductiveVal) (pats : Array CasesPattern) (imode? : Option IndexingMode) (md indexMd : Lean.Meta.TransparencyMode) (phase : PhaseSpec) : Lean.MetaM LocalRuleSetMember

decl is either the name of the inductive type described by info, or a type synonym for it at transparency default or md (whichever is larger).

def Aesop.RuleBuilder.cases : RuleBuilder