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

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

• Lean.Meta.Match.MatcherInfo.numAlts info = Array.size info.altNumParams

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

Equations

• Lean.Meta.Match.MatcherInfo.arity info = info.numParams + 1 + info.numDiscrs + Lean.Meta.Match.MatcherInfo.numAlts info

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

Equations

• Lean.Meta.Match.MatcherInfo.getFirstDiscrPos info = info.numParams + 1

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

Equations

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

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

Equations

• Lean.Meta.Match.MatcherInfo.getFirstAltPos info = info.numParams + 1 + info.numDiscrs

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

Equations

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

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

Equations

• Lean.Meta.Match.MatcherInfo.getMotivePos info = info.numParams

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

Equations

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

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

Equations

• Lean.Meta.Match.MatcherInfo.getNumDiscrEqs info = Lean.Meta.Match.getNumEqsFromDiscrInfos info.discrInfos

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

Equations

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

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

Equations

• Lean.Meta.Match.Extension.State.addEntry s e = { map := Lean.SMap.insert s.map e.name e.info }

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

Equations

• Lean.Meta.Match.Extension.State.switch s = { map := Lean.SMap.switch s.map }

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

Equations

• Lean.Meta.Match.Extension.addMatcherInfo env matcherName info = Lean.PersistentEnvExtension.addEntry Lean.Meta.Match.Extension.extension env { name := matcherName, info := info }

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

Equations

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

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

Equations

• Lean.Meta.Match.addMatcherInfo matcherName info = Lean.modifyEnv fun (env : Lean.Environment) => Lean.Meta.Match.Extension.addMatcherInfo env matcherName info

def Lean.Meta.getMatcherInfoCore? (env : Lean.Environment) (declName : Lake.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 : Lake.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 : Lake.Name) : Bool

Equations

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

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

Equations

• Lean.Meta.isMatcher declName = do let __do_lift ← Lean.getEnv pure (Lean.Meta.isMatcherCore __do_lift declName)

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

Equations

• Lean.Meta.isMatcherAppCore env e = Option.isSome (Lean.Meta.isMatcherAppCore? env e)

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)

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)

Equations

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

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

Equations

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