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

def Aesop.RuleTac.cases.findFirstApplicableHyp (target : CasesTarget) (md : Lean.Meta.TransparencyMode) (excluded : Array Lean.FVarId) (goal : Lean.MVarId) : Lean.MetaM (Option Lean.FVarId)

partial def Aesop.RuleTac.cases.go (target : CasesTarget) (md : Lean.Meta.TransparencyMode) (isRecursiveType : Bool) (ctorNames : Array CtorNames) (initialGoal : Lean.MVarId) (newGoals : Array Subgoal) (excluded : Array Lean.FVarId) (goal : Lean.MVarId) : ScriptM (Option (Array Subgoal))