def Lean.Meta.MatcherApp.addArg (matcherApp : Lean.Meta.MatcherApp) (e : Lean.Expr) : Lean.MetaM Lean.Meta.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 use kabstract to abstract the discriminants from B[discrs].

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 the termination argument, which may mention major. See there for how to use this function.

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

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

Equations

• matcherApp.addArg? e = do let r ← tryCatch (do let __do_lift ← matcherApp.addArg e pure (some __do_lift)) fun (x : Lean.Exception) => pure none pure r

def Lean.Meta.MatcherApp.refineThrough (matcherApp : Lean.Meta.MatcherApp) (e : Lean.Expr) : Lean.MetaM (Array Lean.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.

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

A non-failing version of MatcherApp.refineThrough

def Lean.Meta.MatcherApp.withUserNames {n : Type → Type u_1} [MonadControlT Lean.MetaM n] [Monad n] {α : Type} (fvars : Array Lean.Expr) (names : Array Lean.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

def Lean.Meta.MatcherApp.transform {n : Type → Type} [MonadLiftT Lean.MetaM n] [MonadControlT Lean.MetaM n] [Monad n] [Lean.MonadError n] [Lean.MonadEnv n] [Lean.MonadLog n] [Lean.AddMessageContext n] [Lean.MonadOptions n] (matcherApp : Lean.Meta.MatcherApp) (useSplitter addEqualities : Bool := false) (onParams : Lean.Expr → n Lean.Expr := pure) (onMotive : Array Lean.Expr → Lean.Expr → n Lean.Expr := fun (x : Array Lean.Expr) (e : Lean.Expr) => pure e) (onAlt : Lean.Expr → Lean.Expr → n Lean.Expr := fun (x e : Lean.Expr) => pure e) (onRemaining : Array Lean.Expr → n (Array Lean.Expr) := pure) : n Lean.Meta.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.

def Lean.Meta.MatcherApp.inferMatchType (matcherApp : Lean.Meta.MatcherApp) : Lean.MetaM Lean.Meta.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.