structure Lean.Meta.Match.DiscrInfo : Type

• hName? : Option Lean.Name

  some h if the discriminant is annotated with h:

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

Equations

• Lean.Meta.Match.instInhabitedDiscrInfo = { default := { hName? := default } }

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 Lean.Meta.Match.DiscrInfo

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

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

Equations

• info.numAlts = info.altNumParams.size

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

Equations

• info.arity = info.numParams + 1 + info.numDiscrs + info.numAlts

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

Equations

• info.getMotivePos = info.numParams

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 : Lean.Name
• info : Lean.Meta.MatcherInfo

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

• map : Lean.SMap Lean.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 : Lean.Name) (info : Lean.Meta.MatcherInfo) : Lean.Environment

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

Equations

• Lean.Meta.Match.Extension.getMatcherInfo? env declName = (Lean.Meta.Match.Extension.extension.getState env).map.find? declName

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

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

Equations

• Lean.Meta.getMatcherInfoCore? env declName = Lean.Meta.Match.Extension.getMatcherInfo? env declName

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

Equations

• Lean.Meta.getMatcherInfo? declName = do let __do_lift ← Lean.getEnv pure (Lean.Meta.getMatcherInfoCore? __do_lift declName)

@[export lean_is_matcher]

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

Equations

• Lean.Meta.isMatcherCore env declName = (Lean.Meta.getMatcherInfoCore? env declName).isSome

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

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

Equations

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

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

Equations

• Lean.Meta.isMatcherApp e = do let __do_lift ← Lean.getEnv pure (Lean.Meta.isMatcherAppCore __do_lift e)