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

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

@[implicit_reducible]

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.expr : SplitInfo → Expr

The expression represented by a SplitInfo.

def Lean.Elab.Tactic.Do.SplitInfo.withAbstract {n : Type → Type u_1} {α : Type} [MonadLiftT MetaM n] [MonadControlT MetaM n] [Monad n] [Inhabited α] (info : SplitInfo) (resTy : Expr) (k : SplitInfo → Array Expr → n α) : n α

Introduces fvars for all varying parts of a SplitInfo and provides the abstract SplitInfo and fvars to the continuation.

For ite/dite, introduces c : Prop, dec : Decidable c, t : mα (or t : c → mα), e : mα (or e : ¬c → mα). For matcher, introduces discriminant fvars and alternative fvars, builds a non-dependent motive fun _ ... _ => mα, and adjusts matcher universe levels.

The abstract SplitInfo satisfies abstractInfo.expr = abstractProgram.

For matcher, the abstract MatcherApp stores eta-expanded fvar alts so that splitWith/matcherApp.transform can instantiateLambda them directly (no patching needed). Since eta-expanded alts like fun n => alt n can cause expensive higher-order unification in backward rule patterns, callers building backward rules should eta-reduce them first (e.g. via Expr.eta on the alt arguments of abstractInfo.expr).

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 → Meta.MatcherApp.TransformAltFVars → 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