Documentation

Lean.Meta.Match.MatcherInfo

structure Lean.Meta.Match.DiscrInfo:

Type

some h if the discriminant is annotated with h:
hName? : Option Lean.Name

instance Lean.Meta.Match.instInhabitedDiscrInfo:

Inhabited Lean.Meta.Match.DiscrInfo

Equations

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

structure Lean.Meta.Match.MatcherInfo:

Type

numParams : Nat
numDiscrs : Nat
altNumParams : Array Nat
uElimPos? : Option Nat
discrInfos[i] = { hName? := some h } if the i-th discriminant was annotated with h :.
discrInfos : Array Lean.Meta.Match.DiscrInfo

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) :

Equations

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

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

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) :

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

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

Lean.MetaM Unit

Equations

Lean.Meta.Match.addMatcherInfo matcherName info = Lean.modifyEnv fun env => Lean.Meta.Match.Extension.addMatcherInfo env matcherName info

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} [inst : Monad m] [inst : Lean.MonadEnv m] (declName : Lean.Name) :

m (Option Lean.Meta.MatcherInfo)

Equations

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

@[export lean_is_matcher]

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

Equations

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

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

Equations

Lean.Meta.isMatcher declName = do let a ← Lean.getEnv pure (Lean.Meta.isMatcherCore a 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) :

Equations

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

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

Equations

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

structure Lean.Meta.MatcherApp:

Type

matcherName : Lean.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} [inst : Monad m] [inst : 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) :

Equations

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