structure Lean.Meta.Match.DiscrInfo : Type

• hName? : Option Name

  some h if the discriminant is annotated with h:

@[implicit_reducible]

instance Lean.Meta.Match.instInhabitedDiscrInfo : Inhabited DiscrInfo

def Lean.Meta.Match.instInhabitedDiscrInfo.default : DiscrInfo

def Lean.Meta.Match.instReprDiscrInfo.repr : DiscrInfo → Nat → Format

@[implicit_reducible]

instance Lean.Meta.Match.instReprDiscrInfo : Repr DiscrInfo

structure Lean.Meta.Match.Overlaps : Type

• map : Std.HashMap Nat (Std.TreeSet Nat compare)

@[implicit_reducible]

instance Lean.Meta.Match.instInhabitedOverlaps : Inhabited Overlaps

def Lean.Meta.Match.instInhabitedOverlaps.default : Overlaps

@[implicit_reducible]

instance Lean.Meta.Match.instReprOverlaps : Repr Overlaps

def Lean.Meta.Match.instReprOverlaps.repr : Overlaps → Nat → Format

def Lean.Meta.Match.Overlaps.isEmpty (o : Overlaps) : Bool

def Lean.Meta.Match.Overlaps.insert (o : Overlaps) (overlapping overlapped : Nat) : Overlaps

def Lean.Meta.Match.Overlaps.overlapping (o : Overlaps) (overlapped : Nat) : Array Nat

structure Lean.Meta.Match.AltParamInfo : Type

Information about the parameter structure for the alternative of a matcher or splitter.

• numFields : Nat

  Actual fields (not including discr eqns)

• numOverlaps : Nat

  Overlap assumption (for splitters only)

• hasUnitThunk : Bool

  Whether this alternative has an artificial Unit parameter

@[implicit_reducible]

instance Lean.Meta.Match.instInhabitedAltParamInfo : Inhabited AltParamInfo

def Lean.Meta.Match.instInhabitedAltParamInfo.default : AltParamInfo

@[implicit_reducible]

instance Lean.Meta.Match.instReprAltParamInfo : Repr AltParamInfo

def Lean.Meta.Match.instReprAltParamInfo.repr : AltParamInfo → Nat → Format

@[implicit_reducible]

instance Lean.Meta.Match.instBEqAltParamInfo : BEq AltParamInfo

def Lean.Meta.Match.instBEqAltParamInfo.beq : AltParamInfo → AltParamInfo → Bool

structure Lean.Meta.Match.MatcherInfo : Type

Information about the structure of a matcher declaration

• numParams : Nat

  Number of parameters

• numDiscrs : Nat

  Number of discriminants

• altInfos : Array AltParamInfo

  Parameter structure information for each alternative

• uElimPos? : Option Nat

  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.

• discrInfos : Array DiscrInfo

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

• overlaps : Overlaps

  (Conservative approximation of) which alternatives may overlap another.

def Lean.Meta.Match.instInhabitedMatcherInfo.default : MatcherInfo

@[implicit_reducible]

instance Lean.Meta.Match.instInhabitedMatcherInfo : Inhabited MatcherInfo

def Lean.Meta.Match.instReprMatcherInfo.repr : MatcherInfo → Nat → Format

@[implicit_reducible]

instance Lean.Meta.Match.instReprMatcherInfo : Repr MatcherInfo

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

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

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

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

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

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

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

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

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

def Lean.Meta.Match.MatcherInfo.altNumParams (info : MatcherInfo) : Array Nat

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

• name : Name
• info : MatcherInfo

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

• map : SMap Name MatcherInfo

@[implicit_reducible]

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

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

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

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

def Lean.Meta.Match.Extension.addMatcherInfo (env : Environment) (matcherName : Name) (info : MatcherInfo) : Environment

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

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

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

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

@[export lean_is_matcher]

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

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

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

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

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

opaque Lean.Meta.matcherLikeExt : TagDeclarationExtension

Tag extension for declarations that should be inlined like matchers during LCNF conversion, but are not matchers themselves (e.g. the .het auxiliaries from mkCasesOnSameCtor).

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

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

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