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

Instances For

source
def Lean.Meta.MatcherApp.addArg? (matcherApp : MatcherApp) (e : Expr) :
MetaM (Option 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

Instances For

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

Instances For

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

Instances For

source
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

Instances For

source
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 → Array Expr → Expr → n Expr := fun (x : Nat) (x_1 : Expr) (x_2 : Array Expr) (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.

Instances For

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

Instances For