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

Equations

• Lean.Meta.Match.instInhabitedMatchEqns = { default := { eqnNames := default, splitterName := default, splitterAltNumParams := default } }

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

Equations

• Lean.Meta.Match.MatchEqns.size e = Array.size e.eqnNames

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

Equations

• Lean.Meta.Match.instInhabitedMatchEqnsExtState = { default := { map := default } }

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

Equations

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

@[extern lean_get_match_equations_for]

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