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

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

Instances For

source
instance Lean.Elab.Tactic.Do.instInhabitedSplitInfo :
Inhabited SplitInfo
Equations

- Lean.Elab.Tactic.Do.instInhabitedSplitInfo = { default := Lean.Elab.Tactic.Do.instInhabitedSplitInfo.default }

source
def Lean.Elab.Tactic.Do.instInhabitedSplitInfo.default :
SplitInfo
Equations

- Lean.Elab.Tactic.Do.instInhabitedSplitInfo.default = Lean.Elab.Tactic.Do.SplitInfo.ite default

Instances For

source
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)

Instances For

source
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

Instances For

source
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.

Instances For

source
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

Instances For

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

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

Instances For

source
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.

Instances For