def Lean.Meta.Split.getSimpMatchContext : MetaM Simp.Context

def Lean.Meta.Split.simpMatch (e : Expr) : MetaM Simp.Result

def Lean.Meta.Split.simpMatchTarget (mvarId : MVarId) : MetaM MVarId

opaque Lean.Meta.Split.discrGenExId : InternalExceptionId

Internal exception for discriminant generalization failures due to type errors.

def Lean.Meta.Split.isDiscrGenException (ex : Exception) : Bool

def Lean.Meta.Split.applyMatchSplitter (mvarId : MVarId) (matcherDeclName : Name) (us : Array Level) (params discrs : Array Expr) : MetaM (List MVarId)

def Lean.Meta.Split.mkDiscrGenErrorMsg (e : Expr) : MessageData

def Lean.Meta.Split.throwDiscrGenError {α : Type} (e : Expr) : MetaM α

def Lean.Meta.Split.splitMatch (mvarId : MVarId) (e : Expr) : MetaM (List MVarId)

def Lean.Meta.splitTarget? (mvarId : MVarId) (splitIte : Bool := true) (useNewSemantics : Bool := false) : MetaM (Option (List MVarId))

Splits an if-then-else of match-expression in the goal target. If useNewSemantics is true, the flag backward.split is ignored. Recall this flag only affects the split of if-then-else expressions.

def Lean.Meta.splitLocalDecl? (mvarId : MVarId) (fvarId : FVarId) : MetaM (Option (List MVarId))