structure Lean.Meta.Match.MatchEqns : Type

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

instance Lean.Meta.Match.instInhabitedMatchEqns : Inhabited MatchEqns

instance Lean.Meta.Match.instReprMatchEqns : Repr MatchEqns

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

structure Lean.Meta.Match.MatchEqnsExtState : Type

• map : PHashMap Name MatchEqns
• eqns : PHashSet Name

instance Lean.Meta.Match.instInhabitedMatchEqnsExtState : Inhabited MatchEqnsExtState

opaque Lean.Meta.Match.matchEqnsExt : EnvExtension MatchEqnsExtState

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

@[extern lean_get_match_equations_for]

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

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

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