structure Lean.Meta.Match.DiscrInfo : Type

• hName? : Option Name

  some h if the discriminant is annotated with h:

Instances For

• Lean.Meta.Match.instInhabitedDiscrInfo

instance Lean.Meta.Match.instInhabitedDiscrInfo : Inhabited 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 DiscrInfo

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

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

Equations

• info.numAlts = info.altNumParams.size

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

Equations

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

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

Equations

• info.getFirstDiscrPos = info.numParams + 1

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

• info.getMotivePos = info.numParams

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

Equations

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

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

Equations

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

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

• name : Name
• info : MatcherInfo

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

• map : SMap Name MatcherInfo

Instances For

• Lean.Meta.Match.Extension.instInhabitedState

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

Equations

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

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

Equations

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

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

Equations

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

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

def Lean.Meta.Match.Extension.addMatcherInfo (env : Environment) (matcherName : Name) (info : MatcherInfo) : 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 : Environment) (declName : Name) : Option 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] [MonadEnv m] (matcherName : Name) (info : 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 : Environment) (declName : Name) : Option MatcherInfo

Equations

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

def Lean.Meta.getMatcherInfo? {m : Type → Type} [Monad m] [MonadEnv m] (declName : Name) : m (Option 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 : Environment) (declName : Name) : Bool

Equations

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

def Lean.Meta.isMatcher {m : Type → Type} [Monad m] [MonadEnv m] (declName : 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 : Environment) (e : Expr) : Option MatcherInfo

Equations

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

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

Equations

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

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

Equations

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