structure Lean.Meta.Match.MatchEqns : Type

• eqnNames : Array Name
• splitterName : Name
• splitterMatchInfo : MatcherInfo

@[implicit_reducible]

instance Lean.Meta.Match.instInhabitedMatchEqns : Inhabited MatchEqns

def Lean.Meta.Match.instInhabitedMatchEqns.default : MatchEqns

def Lean.Meta.Match.instReprMatchEqns.repr : MatchEqns → Nat → Format

@[implicit_reducible]

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

def Lean.Meta.Match.instInhabitedMatchEqnsExtState.default : MatchEqnsExtState

@[implicit_reducible]

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

@[extern lean_get_congr_match_equations_for]

opaque Lean.Meta.Match.genMatchCongrEqns (matchDeclName : Name) : MetaM (Array Name)

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

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