structure Lean.Meta.Match.MatchEqns : Type

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

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

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

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

structure Lean.Meta.Match.MatchEqnsExtState : Type

• map : Lean.PHashMap Lake.Name Lean.Meta.Match.MatchEqns

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 : Lake.Name) (matchEqns : Lean.Meta.Match.MatchEqns) : Lean.CoreM Unit

@[extern lean_get_match_equations_for]

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