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 (info : Lean.InductiveVal) (pats : Array CasesPattern) (imode? : Option IndexingMode) (md indexMd : Lean.Meta.TransparencyMode) (phase : PhaseSpec) : Lean.MetaM LocalRuleSetMember

def Aesop.RuleBuilder.cases : RuleBuilder