structure Lean.Meta.Match.DiscrInfo : Type

• hName? : Option Name

  some h if the discriminant is annotated with h:

instance Lean.Meta.Match.instInhabitedDiscrInfo : Inhabited DiscrInfo

structure Lean.Meta.Match.MatcherInfo : Type

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.

• numParams : Nat
• numDiscrs : Nat
• altNumParams : Array Nat
• uElimPos? : Option Nat
• discrInfos : Array DiscrInfo

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

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

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

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

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

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

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

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

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

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

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

• name : Name
• info : MatcherInfo

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

• map : SMap Name MatcherInfo

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

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

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

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

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

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

def Lean.Meta.Match.addMatcherInfo {m : Type → Type} [Monad m] [MonadEnv m] (matcherName : Name) (info : MatcherInfo) : m Unit

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

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

@[export lean_is_matcher]

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

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

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

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

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