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

Equations

• Lean.Elab.Tactic.Do.instInhabitedSplitInfo = { default := Lean.Elab.Tactic.Do.SplitInfo.ite default }

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

Equations

• One or more equations did not get rendered due to their size.
• (Lean.Elab.Tactic.Do.SplitInfo.ite e).resTy = some (e.getArg! 0)
• (Lean.Elab.Tactic.Do.SplitInfo.dite e).resTy = some (e.getArg! 0)

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.

Equations

• (Lean.Elab.Tactic.Do.SplitInfo.ite e).altInfos = #[(0, e.getArg! 3), (0, e.getArg! 4)]
• (Lean.Elab.Tactic.Do.SplitInfo.dite e).altInfos = #[(1, e.getArg! 3), (1, e.getArg! 4)]
• (Lean.Elab.Tactic.Do.SplitInfo.matcher matcherApp).altInfos = Array.mapIdx (fun (idx numParams : Nat) => (numParams, matcherApp.alts[idx]!)) matcherApp.altNumParams

def Lean.Elab.Tactic.Do.SplitInfo.splitWithConstantMotive {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 → Nat → Array Expr → n Expr) (useSplitter : Bool := false) : n Expr

Equations

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

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

Equations

• (Lean.Elab.Tactic.Do.SplitInfo.dite e_1).simpDiscrs? e = pure none
• (Lean.Elab.Tactic.Do.SplitInfo.ite e_1).simpDiscrs? e = pure none
• (Lean.Elab.Tactic.Do.SplitInfo.matcher matcherApp).simpDiscrs? e = Lean.Meta.Simp.simpMatchDiscrs? matcherApp.toMatcherInfo e

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

Equations

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

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

Equations

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