structure Lean.Meta.Match.DiscrInfo : Type

• hName? : Option Lake.Name

  some h if the discriminant is annotated with h:

instance Lean.Meta.Match.instInhabitedDiscrInfo : Inhabited Lean.Meta.Match.DiscrInfo

structure Lean.Meta.Match.MatcherInfo : Type

• numParams : Nat
• numDiscrs : Nat
• altNumParams : Array Nat
• uElimPos? : Option Nat
• discrInfos : Array Lean.Meta.Match.DiscrInfo

  discrInfos[i] = { hName? := some h } if the i-th discriminant was annotated with h :.

A "matcher" auxiliary declaration has the following structure:

• numParams parameters
• motive
• numDiscrs discriminators (aka major premises)
• altNumParams.size alternatives (aka minor premises) where alternative i has altNumParams[i] parameters
• uElimPos? is some pos when the matcher can eliminate in different universe levels, and pos is the position of the universe level parameter that specifies the elimination universe. It is none if the matcher only eliminates into Prop.

def Lean.Meta.Match.MatcherInfo.numAlts (info : Lean.Meta.MatcherInfo) : Nat

def Lean.Meta.Match.MatcherInfo.arity (info : Lean.Meta.MatcherInfo) : Nat

def Lean.Meta.Match.MatcherInfo.getFirstDiscrPos (info : Lean.Meta.MatcherInfo) : Nat

def Lean.Meta.Match.MatcherInfo.getDiscrRange (info : Lean.Meta.MatcherInfo) : Std.Range

def Lean.Meta.Match.MatcherInfo.getFirstAltPos (info : Lean.Meta.MatcherInfo) : Nat

def Lean.Meta.Match.MatcherInfo.getAltRange (info : Lean.Meta.MatcherInfo) : Std.Range

def Lean.Meta.Match.MatcherInfo.getMotivePos (info : Lean.Meta.MatcherInfo) : Nat

def Lean.Meta.Match.getNumEqsFromDiscrInfos (infos : Array Lean.Meta.Match.DiscrInfo) : Nat

def Lean.Meta.Match.MatcherInfo.getNumDiscrEqs (info : Lean.Meta.MatcherInfo) : Nat

structure Lean.Meta.Match.Extension.Entry : Type

• name : Lake.Name
• info : Lean.Meta.MatcherInfo

structure Lean.Meta.Match.Extension.State : Type

• map : Lean.SMap Lake.Name Lean.Meta.MatcherInfo

instance Lean.Meta.Match.Extension.instInhabitedState : Inhabited Lean.Meta.Match.Extension.State

def Lean.Meta.Match.Extension.State.addEntry (s : Lean.Meta.Match.Extension.State) (e : Lean.Meta.Match.Extension.Entry) : Lean.Meta.Match.Extension.State

def Lean.Meta.Match.Extension.State.switch (s : Lean.Meta.Match.Extension.State) : Lean.Meta.Match.Extension.State

opaque Lean.Meta.Match.Extension.extension : Lean.SimplePersistentEnvExtension Lean.Meta.Match.Extension.Entry Lean.Meta.Match.Extension.State

def Lean.Meta.Match.Extension.addMatcherInfo (env : Lean.Environment) (matcherName : Lake.Name) (info : Lean.Meta.MatcherInfo) : Lean.Environment

def Lean.Meta.Match.Extension.getMatcherInfo? (env : Lean.Environment) (declName : Lake.Name) : Option Lean.Meta.MatcherInfo

def Lean.Meta.Match.addMatcherInfo (matcherName : Lake.Name) (info : Lean.Meta.MatcherInfo) : Lean.MetaM Unit

def Lean.Meta.getMatcherInfoCore? (env : Lean.Environment) (declName : Lake.Name) : Option Lean.Meta.MatcherInfo

def Lean.Meta.getMatcherInfo? {m : Type → Type} [Monad m] [Lean.MonadEnv m] (declName : Lake.Name) : m (Option Lean.Meta.MatcherInfo)

@[export lean_is_matcher]

def Lean.Meta.isMatcherCore (env : Lean.Environment) (declName : Lake.Name) : Bool

def Lean.Meta.isMatcher {m : Type → Type} [Monad m] [Lean.MonadEnv m] (declName : Lake.Name) : m Bool

def Lean.Meta.isMatcherAppCore? (env : Lean.Environment) (e : Lean.Expr) : Option Lean.Meta.MatcherInfo

def Lean.Meta.isMatcherAppCore (env : Lean.Environment) (e : Lean.Expr) : Bool

def Lean.Meta.isMatcherApp {m : Type → Type} [Monad m] [Lean.MonadEnv m] (e : Lean.Expr) : m Bool

structure Lean.Meta.MatcherApp : Type

• matcherName : Lake.Name
• matcherLevels : Array Lean.Level
• uElimPos? : Option Nat
• params : Array Lean.Expr
• motive : Lean.Expr
• discrs : Array Lean.Expr
• altNumParams : Array Nat
• alts : Array Lean.Expr
• remaining : Array Lean.Expr

def Lean.Meta.matchMatcherApp? {m : Type → Type} [Monad m] [Lean.MonadEnv m] (e : Lean.Expr) : m (Option Lean.Meta.MatcherApp)

def Lean.Meta.MatcherApp.toExpr (matcherApp : Lean.Meta.MatcherApp) : Lean.Expr