inductive Lean.Meta.SplitKind : Type

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

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

Equations

• Lean.Meta.SplitKind.ite.considerIte = true
• Lean.Meta.SplitKind.both.considerIte = true
• x✝.considerIte = false

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

Equations

• Lean.Meta.SplitKind.match.considerMatch = true
• Lean.Meta.SplitKind.both.considerMatch = true
• x✝.considerMatch = false

structure Lean.Meta.FindSplitImpl.Context : Type

• exceptionSet : ExprSet
• kind : SplitKind

@[reducible, inline]

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

Equations

• Lean.Meta.FindSplitImpl.FindM = ReaderT Lean.Meta.FindSplitImpl.Context (StateT (Lean.PtrSet Lean.Expr) Lean.MetaM)

@[inline]

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• Lean.Meta.findSplit? e kind exceptionSet = do let __do_lift ← Lean.instantiateMVars e Lean.Meta.findSplit?.go✝ kind exceptionSet __do_lift

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.

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Lean.Meta.SplitIf.mkDischarge? useDecide = do let __do_lift ← Lean.getLCtx pure (Lean.Meta.SplitIf.discharge?✝ __do_lift.numIndices useDecide)

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

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.