def Lean.Meta.MatcherApp.addArg (matcherApp : MatcherApp) (e : Expr) : MetaM MatcherApp

Given

• matcherApp match_i As (fun xs => motive[xs]) discrs (fun ys_1 => (alt_1 : motive (C_1[ys_1])) ... (fun ys_n => (alt_n : motive (C_n[ys_n]) remaining, and
• expression e : B[discrs], Construct the term match_i As (fun xs => B[xs] -> motive[xs]) discrs (fun ys_1 (y : B[C_1[ys_1]]) => alt_1) ... (fun ys_n (y : B[C_n[ys_n]]) => alt_n) e remaining.

We only abstract discriminants that are fvars. We used to use kabstract to abstract all discriminants from B[discrs], but that changes the type of the arg in ways that make it no longer compatible with the original recursive function (issue #7322).

If this is still not great, then we could try to use kabstract, but only on the last parameter of the arg (the termination proof obligation).

This method assumes

• the matcherApp.motive is a lambda abstraction where xs.size == discrs.size
• each alternative is a lambda abstraction where ys_i.size == matcherApp.altNumParams[i]

This is used in Lean.Elab.PreDefinition.WF.Fix when replacing recursive calls with calls to the argument provided by fix to refine type of the local variable used for recursive calls, which may mention major. See there for how to use this function.

Equations

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

def Lean.Meta.MatcherApp.addArg? (matcherApp : MatcherApp) (e : Expr) : MetaM (Option MatcherApp)

Similar to MatcherApp.addArg, but returns none on failure.

Equations

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

def Lean.Meta.MatcherApp.refineThrough (matcherApp : MatcherApp) (e : Expr) : MetaM (Array Expr)

Given

• matcherApp match_i As (fun xs => motive[xs]) discrs (fun ys_1 => (alt_1 : motive (C_1[ys_1])) ... (fun ys_n => (alt_n : motive (C_n[ys_n]) remaining, and
• a expression B[discrs] (which may not be a type, e.g. n : Nat), returns the expressions fun ys_1 ... ys_i => B[C_1[ys_1]] ... B[C_n[ys_n]],

This method assumes

• the matcherApp.motive is a lambda abstraction where xs.size == discrs.size
• each alternative is a lambda abstraction where ys_i.size == matcherApp.altNumParams[i]

This is similar to MatcherApp.addArg when you only have an expression to refined, and not a type with a value.

This is used in Lean.Elab.PreDefinition.WF.GuessFix when constructing the context of recursive calls to refine the functions' parameter, which may mention major. See there for how to use this function.

Equations

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

def Lean.Meta.MatcherApp.refineThrough? (matcherApp : MatcherApp) (e : Expr) : MetaM (Option (Array Expr))

A non-failing version of MatcherApp.refineThrough

Equations

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

def Lean.Meta.MatcherApp.withUserNames {n : Type → Type u_1} [MonadControlT MetaM n] [Monad n] {α : Type} (fvars : Array Expr) (names : Array Name) (k : n α) : n α

Sets the user name of the FVars in the local context according to the given array of names.

If they differ in size the shorter size wins.

Equations

• Lean.Meta.MatcherApp.withUserNames fvars names k = Lean.Meta.mapMetaM (fun {α : Type} => Lean.Meta.MatcherApp.withUserNamesImpl✝ fvars names) k

structure Lean.Meta.MatcherApp.TransformAltFVars : Type

Fvars/exprs introduced in the telescope of a matcher alternative during transform.

• args are the values passed to instantiateLambda on the original alt. They usually coincide with fields, but may include non-fvar values (e.g. Unit.unit for thunked alts).
• fields are the constructor-field fvars (proper fvar subset of args).
• overlaps are overlap-parameter fvars (splitter path only, for non-casesOn splitters).
• discrEqs are discriminant-equation fvars from the matcher's own type (numDiscrEqs).
• extraEqs are equation fvars added by the addEqualities flag.

Example. transform with addEqualities := true on a Nat.casesOn application Nat.casesOn (motive := …) n alt₀ alt₁ opens alt telescopes:

Alt 0 (zero):  (heq : n = Nat.zero) → motive Nat.zero
  ⟹ { args := #[], fields := #[], extraEqs := #[heq] }

Alt 1 (succ):  (k : Nat) → (heq : n = Nat.succ k) → motive (Nat.succ k)
  ⟹ { args := #[k], fields := #[k], extraEqs := #[heq] }

• args : Array Expr

  Arguments for instantiateLambda on the original alternative (see example above). May include non-fvar values like Unit.unit for thunked alternatives.

• fields : Array Expr

  Constructor field fvars, i.e. the proper fvar subset of args (see example above).

• overlaps : Array Expr

  Overlap parameter fvars (non-casesOn splitters only).

• discrEqs : Array Expr

  Discriminant equation fvars from the matcher's own type (numDiscrEqs).

• extraEqs : Array Expr

  Extra equation fvars added by addEqualities (see heq in the example above).

def Lean.Meta.MatcherApp.TransformAltFVars.altParams (fvars : TransformAltFVars) : Array Expr

The altParams that were used for instantiateLambda alt altParams inside transform.

Equations

• fvars.altParams = fvars.args ++ fvars.discrEqs

def Lean.Meta.MatcherApp.TransformAltFVars.all (fvars : TransformAltFVars) : Array Expr

All proper fvars in binding order, matching the lambdas that transform wraps around the alt result.

Equations

• fvars.all = fvars.fields ++ fvars.overlaps ++ fvars.discrEqs ++ fvars.extraEqs

def Lean.Meta.MatcherApp.transform {n : Type → Type} [MonadLiftT MetaM n] [MonadControlT MetaM n] [Monad n] [MonadError n] [MonadEnv n] [MonadLog n] [AddMessageContext n] [MonadOptions n] (matcherApp : MatcherApp) (useSplitter addEqualities : Bool := false) (onParams : Expr → n Expr := pure) (onMotive : Array Expr → Expr → n Expr := fun (x : Array Expr) (e : Expr) => pure e) (onAlt : Nat → Expr → TransformAltFVars → Expr → n Expr := fun (x : Nat) (x_1 : Expr) (x_2 : TransformAltFVars) (e : Expr) => pure e) (onRemaining : Array Expr → n (Array Expr) := pure) : n MatcherApp

Performs a possibly type-changing transformation to a MatcherApp.

• onParams is run on each parameter and discriminant
• onMotive runs on the body of the motive, and is passed the motive parameters (one for each MatcherApp.discrs)
• onAlt runs on each alternative, and is passed the expected type of the alternative, as inferred from the motive
• onRemaining runs on the remaining arguments (and may change their number)

If useSplitter is true, the matcher is replaced with the splitter. NB: Not all operations on MatcherApp can handle one matcherName is a splitter.

If addEqualities is true, then equalities connecting the discriminant to the parameters of the alternative (like in match h : x with …) are be added, if not already there.

This function works even if the type of alternatives do not fit the inferred type. This allows you to post-process the MatcherApp with MatcherApp.inferMatchType, which will infer a type, given all the alternatives.

Equations

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

def Lean.Meta.MatcherApp.inferMatchType (matcherApp : MatcherApp) : MetaM MatcherApp

Given a MatcherApp, replaces the motive with one that is inferred from the actual types of the alternatives.

For example, given

(match (motive := Nat → Unit → ?) n with
 0 => 1
 _ => true) ()

(for any ?; the motive’s result type be ignored) will give this type

(match n with
 | 0 => Nat
 | _ => Bool)

The given MatcherApp must not use a splitter in matcherName. The resulting expression will use the splitter corresponding to matcherName (this is necessary for the construction).

Internally, this needs to reduce the matcher in a given branch; this is done using Split.simpMatchTarget.

Equations

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