inductive Lean.Meta.SplitKind : Type

• ite : SplitKind
• match : SplitKind
• both : SplitKind

def Lean.Meta.SplitKind.considerIte : SplitKind → Bool

def Lean.Meta.SplitKind.considerMatch : SplitKind → Bool

structure Lean.Meta.FindSplitImpl.Context : Type

• exceptionSet : ExprSet
• kind : SplitKind

@[reducible, inline]

unsafe abbrev Lean.Meta.FindSplitImpl.FindM (α : Type) : Type

@[inline]

unsafe def Lean.Meta.FindSplitImpl.checkVisited (e : Expr) : OptionT FindM Unit

unsafe def Lean.Meta.FindSplitImpl.visit (e : Expr) : OptionT FindM Expr

def Lean.Meta.findSplit? (e : Expr) (kind : SplitKind := SplitKind.both) (exceptionSet : ExprSet := ∅) : MetaM (Option Expr)

Return an if-then-else or match-expr to split.

opaque Lean.Meta.backward.split : Lean.Option Bool

def Lean.Meta.SplitIf.getSimpContext : MetaM Simp.Context

The Simp.Context that used to be used with simpIf methods. It contains all congruence theorems, but just the rewriting rules for reducing if expressions. This function is only used when the old split tactic behavior is enabled.

def Lean.Meta.SplitIf.mkDischarge? (useDecide : Bool := false) : MetaM Simp.Discharge

def Lean.Meta.SplitIf.splitIfAt? (mvarId : MVarId) (e : Expr) (hName? : Option Name) : MetaM (Option (ByCasesSubgoal × ByCasesSubgoal))

def Lean.Meta.simpIfTarget (mvarId : MVarId) (useDecide useNewSemantics : Bool := false) : MetaM MVarId

Simplify the if-then-else targeted by the split tactic. If useNewSemantics is true, the flag backward.split is ignored.

def Lean.Meta.simpIfLocalDecl (mvarId : MVarId) (fvarId : FVarId) (useNewSemantics : Bool := false) : MetaM MVarId

Simplify the if-then-else targeted by the split tactic. If useNewSemantics is true, the flag backward.split is ignored.

def Lean.Meta.splitIfTarget? (mvarId : MVarId) (hName? : Option Name := none) (useNewSemantics : Bool := false) : MetaM (Option (ByCasesSubgoal × ByCasesSubgoal))

Split an if-then-else in the goal target. If useNewSemantics is true, the flag backward.split is ignored.

def Lean.Meta.splitIfLocalDecl? (mvarId : MVarId) (fvarId : FVarId) (hName? : Option Name := none) : MetaM (Option (MVarId × MVarId))

Split an if-then-else in the hypothesis fvarId.