structure Lean.Meta.Match.DiscrInfo : Type

• hName? : Option Lake.Name

  some h if the discriminant is annotated with h:

Instances For

• Lean.Meta.Match.instInhabitedDiscrInfo

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

Equations

• info.getFirstDiscrPos = info.numParams + 1

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

Equations

• info.getDiscrRange = { start := info.getFirstDiscrPos, stop := info.getFirstDiscrPos + info.numDiscrs, step := 1 }

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

Equations

• info.getFirstAltPos = info.numParams + 1 + info.numDiscrs

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

Equations

• info.getAltRange = { start := info.getFirstAltPos, stop := info.getFirstAltPos + info.numAlts, step := 1 }

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

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

• info.getNumDiscrEqs = 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

Instances For

• Lean.Meta.Match.Extension.instInhabitedState

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

• s.addEntry e = { map := s.map.insert e.name e.info }

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

Equations

• s.switch = { map := s.map.switch }

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.Meta.Match.Extension.extension.getState env).map.find? declName

def Lean.Meta.Match.addMatcherInfo {m : Type → Type} [Monad m] [Lean.MonadEnv m] (matcherName : Lake.Name) (info : Lean.Meta.MatcherInfo) : m 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 = (Lean.Meta.getMatcherInfoCore? env declName).isSome

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 = (Lean.Meta.isMatcherAppCore? env e).isSome

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)