structure Lean.Meta.Match.MatchEqns : Type

• eqnNames : Array Lean.Name
• splitterName : Lean.Name
• splitterAltNumParams : Array Nat

instance Lean.Meta.Match.instInhabitedMatchEqns : Inhabited Lean.Meta.Match.MatchEqns

instance Lean.Meta.Match.instReprMatchEqns : Repr Lean.Meta.Match.MatchEqns

Equations

• Lean.Meta.Match.instReprMatchEqns = { reprPrec := Lean.Meta.Match.reprMatchEqns✝ }

def Lean.Meta.Match.MatchEqns.size (e : Lean.Meta.Match.MatchEqns) : Nat

structure Lean.Meta.Match.MatchEqnsExtState : Type

• map : Lean.PHashMap Lean.Name Lean.Meta.Match.MatchEqns
• eqns : Lean.PHashSet Lean.Name

instance Lean.Meta.Match.instInhabitedMatchEqnsExtState : Inhabited Lean.Meta.Match.MatchEqnsExtState

opaque Lean.Meta.Match.matchEqnsExt : Lean.EnvExtension Lean.Meta.Match.MatchEqnsExtState

def Lean.Meta.Match.registerMatchEqns (matchDeclName : Lean.Name) (matchEqns : Lean.Meta.Match.MatchEqns) : Lean.CoreM Unit

@[extern lean_get_match_equations_for]

opaque Lean.Meta.Match.getEquationsFor (matchDeclName : Lean.Name) : Lean.MetaM Lean.Meta.Match.MatchEqns

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

Returns true if declName is the name of a match equational theorem.

Equations

• Lean.Meta.Match.isMatchEqnTheorem env declName = Lean.PersistentHashSet.contains (Lean.Meta.Match.matchEqnsExt.getState env).eqns declName