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

Equations

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

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

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

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 in Lean.Elab.PreDefinition.WF.GuessFix when constructing the context of recursive calls to refine the functions' paramter, 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 : Lean.Meta.MatcherApp) (e : Lean.Expr) : Lean.MetaM (Option (Array Lean.Expr))

A non-failing version of MatcherApp.refineThrough

Equations

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