structure Lean.Meta.Match.State : Type

• used : Lean.HashSet Nat
• counterExamples : List (List Lean.Meta.Match.Example)

Note that we decided to store pending constraints to address issues exposed by #1279 and #1361. Here is a simplified version of the example on this issue (see test: 1279_simplified.lean)

inductive Arrow : Type → Type → Type 1
  | id   : Arrow a a
  | unit : Arrow Unit Unit
  | comp : Arrow β γ → Arrow α β → Arrow α γ
deriving Repr

def Arrow.compose (f : Arrow β γ) (g : Arrow α β) : Arrow α γ :=
  match f, g with
  | id, g => g
  | f, id => f
  | f, g => comp f g

The initial state for the match-expression above is

[Meta.Match.match] remaining variables: [β✝:(Type), γ✝:(Type), f✝:(Arrow β✝ γ✝), g✝:(Arrow α β✝)]
alternatives:
  [β:(Type), g:(Arrow α β)] |- [β, .(β), (Arrow.id .(β)), g] => h_1 β g
  [γ:(Type), f:(Arrow α γ)] |- [.(α), γ, f, (Arrow.id .(α))] => h_2 γ f
  [β:(Type), γ:(Type), f:(Arrow β γ), g:(Arrow α β)] |- [β, γ, f, g] => h_3 β γ f g

The first step is a variable-transition which replaces β with β✝ in the first and third alternatives. The constraint β✝ ≋ α in the second alternative used to be discarded. We now store it at the alternative cnstrs field.

def Lean.Meta.Match.processInaccessibleAsCtor (alt : Lean.Meta.Match.Alt) (ctorName : Lake.Name) : Lean.MetaM (Option Lean.Meta.Match.Alt)

Given alt s.t. the next pattern is an inaccessible pattern e, try to normalize e into a constructor application. If it is not a constructor, throw an error. Otherwise, if it is a constructor application of ctorName, update the next patterns with the fields of the constructor. Otherwise, return none.

Equations

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

def Lean.Meta.Match.isCurrVarInductive (p : Lean.Meta.Match.Problem) : Lean.MetaM Bool

Equations

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

opaque Lean.Meta.Match.bootstrap.genMatcherCode : Lean.Option Bool

opaque Lean.Meta.Match.matcherExt : Lean.EnvExtension (Lean.PHashMap (Lean.Expr × Bool) Lake.Name)

def Lean.Meta.Match.mkMatcherAuxDefinition (name : Lake.Name) (type : Lean.Expr) (value : Lean.Expr) : Lean.MetaM (Lean.Expr × Option (Lean.Meta.MatcherInfo → Lean.MetaM Unit))

Similar to mkAuxDefinition, but uses the cache matcherExt. It also returns an Boolean that indicates whether a new matcher function was added to the environment or not.

Equations

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

structure Lean.Meta.Match.MkMatcherInput : Type

• matcherName : Lake.Name
• matchType : Lean.Expr
• discrInfos : Array Lean.Meta.Match.DiscrInfo
• lhss : List Lean.Meta.Match.AltLHS

def Lean.Meta.Match.MkMatcherInput.numDiscrs (m : Lean.Meta.Match.MkMatcherInput) : Nat

Equations

• Lean.Meta.Match.MkMatcherInput.numDiscrs m = Array.size m.discrInfos

def Lean.Meta.Match.MkMatcherInput.collectFVars (m : Lean.Meta.Match.MkMatcherInput) : StateRefT' IO.RealWorld Lean.CollectFVars.State Lean.MetaM Unit

Equations

• Lean.Meta.Match.MkMatcherInput.collectFVars m = do Lean.Expr.collectFVars m.matchType List.forM m.lhss fun (alt : Lean.Meta.Match.AltLHS) => Lean.Meta.Match.AltLHS.collectFVars alt

def Lean.Meta.Match.MkMatcherInput.collectDependencies (m : Lean.Meta.Match.MkMatcherInput) : Lean.MetaM Lean.FVarIdSet

Equations

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

def Lean.Meta.Match.withCleanLCtxFor {α : Type} (m : Lean.Meta.Match.MkMatcherInput) (k : Lean.MetaM α) : Lean.MetaM α

Auxiliary method used at mkMatcher. It executes k in a local context that contains only the local declarations m depends on. This is important because otherwise dependent elimination may "refine" the types of unnecessary declarations and accidentally introduce unnecessary dependencies in the auto-generated auxiliary declaration. Note that this is not just an optimization because the unnecessary dependencies may prevent the termination checker from succeeding. For an example, see issue #1237.

Equations

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

def Lean.Meta.Match.mkMatcher (input : Lean.Meta.Match.MkMatcherInput) : Lean.MetaM Lean.Meta.Match.MatcherResult

Create a dependent matcher for matchType where matchType is of the form (a_1 : A_1) -> (a_2 : A_2[a_1]) -> ... -> (a_n : A_n[a_1, a_2, ... a_{n-1}]) -> B[a_1, ..., a_n] where n = numDiscrs, and the lhss are the left-hand-sides of the match-expression alternatives. Each AltLHS has a list of local declarations and a list of patterns. The number of patterns must be the same in each AltLHS. The generated matcher has the structure described at MatcherInfo. The motive argument is of the form (motive : (a_1 : A_1) -> (a_2 : A_2[a_1]) -> ... -> (a_n : A_n[a_1, a_2, ... a_{n-1}]) -> Sort v) where v is a universe parameter or 0 if B[a_1, ..., a_n] is a proposition.

Equations

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

def Lean.Meta.Match.getMkMatcherInputInContext (matcherApp : Lean.Meta.MatcherApp) : Lean.MetaM Lean.Meta.Match.MkMatcherInput

Equations

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

def Lean.Meta.Match.withMkMatcherInput {α : Type} (matcherName : Lake.Name) (k : Lean.Meta.Match.MkMatcherInput → Lean.MetaM α) : Lean.MetaM α

This function is only used for testing purposes

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