inductive Lean.Elab.Tactic.Do.SplitInfo : Type

• ite (e : Expr) : SplitInfo
• dite (e : Expr) : SplitInfo
• matcher (matcherApp : Meta.MatcherApp) : SplitInfo

instance Lean.Elab.Tactic.Do.instInhabitedSplitInfo : Inhabited SplitInfo

def Lean.Elab.Tactic.Do.instInhabitedSplitInfo.default : SplitInfo

def Lean.Elab.Tactic.Do.SplitInfo.resTy (info : SplitInfo) : Option Expr

def Lean.Elab.Tactic.Do.SplitInfo.altInfos (info : SplitInfo) : Array (Nat × Expr)

A list of pairs (numParams, alt) per match alternative, where numParams is the number of parameters of the alternative and alt is the alternative.

def Lean.Elab.Tactic.Do.SplitInfo.splitWith {n : Type → Type} [MonadLiftT MetaM n] [MonadControlT MetaM n] [Monad n] [MonadError n] [MonadEnv n] [MonadLog n] [AddMessageContext n] [MonadOptions n] (info : SplitInfo) (resTy : Expr) (onAlt : Name → Expr → Nat → Array Expr → n Expr) (useSplitter : Bool := false) : n Expr

def Lean.Elab.Tactic.Do.SplitInfo.simpDiscrs? (info : SplitInfo) (e : Expr) : Meta.SimpM (Option Meta.Simp.Result)

def Lean.Elab.Tactic.Do.getSplitInfo? (e : Expr) : MetaM (Option SplitInfo)

def Lean.Elab.Tactic.Do.rwIfOrMatcher (idx : Nat) (e : Expr) : MetaM Meta.Simp.Result