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

• e.size = e.eqnNames.size

structure Lean.Meta.Match.MatchEqnsExtState : Type

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

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

Equations

• Lean.Meta.Match.instInhabitedMatchEqnsExtState = { default := { map := default, eqns := 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

def Lean.Meta.Match.isMatchEqnTheorem (env : Lean.Environment) (declName : Lake.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