Lean.Elab.Tactic.Do.VCGen.Split

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.expr :

SplitInfo → Expr

The expression represented by a SplitInfo.

Equations

(Lean.Elab.Tactic.Do.SplitInfo.ite e).expr = e
(Lean.Elab.Tactic.Do.SplitInfo.dite e).expr = e
(Lean.Elab.Tactic.Do.SplitInfo.matcher matcherApp).expr = matcherApp.toExpr

Instances For

source

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

Equations