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

Equations

• Lean.Meta.Match.instInhabitedDiscrInfo = { default := Lean.Meta.Match.instInhabitedDiscrInfo.default }

@[implicit_reducible]

instance Lean.Meta.Match.instReprDiscrInfo : Repr DiscrInfo

Equations

• Lean.Meta.Match.instReprDiscrInfo = { reprPrec := Lean.Meta.Match.instReprDiscrInfo.repr }

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

Equations

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

structure Lean.Meta.Match.Overlaps : Type

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

@[implicit_reducible]

instance Lean.Meta.Match.instInhabitedOverlaps : Inhabited Overlaps

Equations

• Lean.Meta.Match.instInhabitedOverlaps = { default := Lean.Meta.Match.instInhabitedOverlaps.default }

@[implicit_reducible]

instance Lean.Meta.Match.instReprOverlaps : Repr Overlaps

Equations

• Lean.Meta.Match.instReprOverlaps = { reprPrec := Lean.Meta.Match.instReprOverlaps.repr }

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

Equations

• Lean.Meta.Match.instReprOverlaps.repr x✝ prec✝ = Std.Format.bracket "{ " (Std.Format.nil ++ Std.Format.text "map" ++ Std.Format.text " := " ++ (Std.Format.nest 7 (repr x✝.map)).group) " }"

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

Equations

• o.isEmpty = o.map.isEmpty

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

Equations

• o.insert overlapping overlapped = { map := o.map.alter overlapped fun (s? : Option (Std.TreeSet Nat compare)) => some ((s?.getD ∅).insert overlapping) }

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

Equations

• o.overlapping overlapped = match o.map[overlapped]? with | some s => s.toArray | none => #[]

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

Equations

• Lean.Meta.Match.instInhabitedAltParamInfo = { default := Lean.Meta.Match.instInhabitedAltParamInfo.default }

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

Equations

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

@[implicit_reducible]

instance Lean.Meta.Match.instReprAltParamInfo : Repr AltParamInfo

Equations

• Lean.Meta.Match.instReprAltParamInfo = { reprPrec := Lean.Meta.Match.instReprAltParamInfo.repr }

@[implicit_reducible]

instance Lean.Meta.Match.instBEqAltParamInfo : BEq AltParamInfo

Equations

• Lean.Meta.Match.instBEqAltParamInfo = { beq := Lean.Meta.Match.instBEqAltParamInfo.beq }

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

Equations

• One or more equations did not get rendered due to their size.
• Lean.Meta.Match.instBEqAltParamInfo.beq x✝¹ x✝ = false

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.

@[implicit_reducible]

instance Lean.Meta.Match.instInhabitedMatcherInfo : Inhabited MatcherInfo

Equations

• Lean.Meta.Match.instInhabitedMatcherInfo = { default := Lean.Meta.Match.instInhabitedMatcherInfo.default }

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

Equations

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

@[implicit_reducible]

instance Lean.Meta.Match.instReprMatcherInfo : Repr MatcherInfo

Equations

• Lean.Meta.Match.instReprMatcherInfo = { reprPrec := Lean.Meta.Match.instReprMatcherInfo.repr }

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

Equations

• info.numAlts = info.altInfos.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.Rco Nat

Equations

• info.getDiscrRange = info.getFirstDiscrPos...info.getFirstDiscrPos + info.numDiscrs

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.Rco Nat

Equations

• info.getAltRange = info.getFirstAltPos...info.getFirstAltPos + info.numAlts

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

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

Equations

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

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

Equations

• Lean.Meta.Match.Extension.instInhabitedState = { default := { } }

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

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

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

Equations

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

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)

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

Equations

• Lean.Meta.markMatcherLike env declName = Lean.Meta.matcherLikeExt.tag env declName

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

Equations

• Lean.Meta.isMatcherLikeCore env declName = Lean.Meta.matcherLikeExt.isTagged env declName

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

Equations

• Lean.Meta.isMatcherLike declName = do let __do_lift ← Lean.getEnv pure (Lean.Meta.isMatcherLikeCore __do_lift declName)