def Lean.Meta.Match.throwIncorrectNumberOfPatternsAt {α : Type} [ToMessageData α] (ref : Syntax) (discrepancyKind : String) (expected actual : Nat) (pats : List α) : MetaM Unit

Throws an error indicating that the alternative at ref contains an unexpected number of patterns. Remark: we allow α to be arbitrary because this error may be thrown before or after elaborating pattern syntax.

def Lean.Meta.Match.logIncorrectNumberOfPatternsAt {α : Type} [ToMessageData α] (ref : Syntax) (discrepancyKind : String) (expected actual : Nat) (pats : List α) : MetaM Unit

Logs an error indicating that the alternative at ref contains an unexpected number of patterns. Remark: we allow α to be arbitrary because this error may be thrown before or after elaborating pattern syntax.

structure Lean.Meta.Match.State : Type

• used : Std.HashSet Nat
• counterExamples : List (List 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 : Alt) (ctorName : Name) : MetaM (Option 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.

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

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

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

def Lean.Meta.Match.mkMatcherAuxDefinition (name : Name) (type value : Expr) : MetaM (Expr × Option (MatcherInfo → 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.

structure Lean.Meta.Match.MkMatcherInput : Type

• matcherName : Name
• matchType : Expr
• discrInfos : Array DiscrInfo
• lhss : List AltLHS

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

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

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

def Lean.Meta.Match.withCleanLCtxFor {α : Type} (m : MkMatcherInput) (k : MetaM α) : 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.

def Lean.Meta.Match.mkMatcher (input : MkMatcherInput) (exceptionIfContainsSorry : Bool := false) : MetaM 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.

If exceptionIfContainsSorry := true, then mkMatcher throws an exception if the auxiliary declarations contains a sorry. We use this argument to workaround a bug at IndPredBelow.mkBelowMatcher.

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

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

This function is only used for testing purposes