structure Lean.Meta.Match.MatchEqns : Type

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

instance Lean.Meta.Match.instInhabitedMatchEqns : Inhabited MatchEqns

Equations

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

instance Lean.Meta.Match.instReprMatchEqns : Repr MatchEqns

Equations

• Lean.Meta.Match.instReprMatchEqns = { reprPrec := Lean.Meta.Match.reprMatchEqns✝ }

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

Equations

• e.size = e.eqnNames.size

structure Lean.Meta.Match.MatchEqnsExtState : Type

• map : PHashMap Name MatchEqns
• eqns : PHashSet Name

instance Lean.Meta.Match.instInhabitedMatchEqnsExtState : Inhabited MatchEqnsExtState

Equations

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

opaque Lean.Meta.Match.matchEqnsExt : EnvExtension MatchEqnsExtState

def Lean.Meta.Match.registerMatchEqns (matchDeclName : Name) (matchEqns : MatchEqns) : 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 : 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.

Equations

• Lean.Meta.Match.isMatchEqnTheorem env declName = Id.run (Lean.PersistentHashSet.contains (Lean.Meta.Match.matchEqnsExt.findStateAsync env declName).eqns declName)