def Aesop.CasesPattern.toExpr (p : CasesPattern) : Lean.MetaM Lean.Expr

inductive Aesop.CasesTarget' : Type

• decl (decl : Lean.Name) : CasesTarget'
• patterns (ps : Array (Lean.Expr × Lean.Meta.SavedState)) : CasesTarget'

def Aesop.CasesTarget.toCasesTarget' : CasesTarget → Lean.MetaM CasesTarget'

def Aesop.RuleTac.cases (target : CasesTarget) (md : Lean.Meta.TransparencyMode) (isRecursiveType : Bool) (ctorNames : Array CtorNames) : RuleTac