Documentation

Lean.Meta.Match.MatchEqsExt

structure Lean.Meta.Match.MatchEqns:

Type

eqnNames : Array Lean.Name
splitterName : Lean.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 := [anonymous] }

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

Equations

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

structure Lean.Meta.Match.MatchEqnsExtState:

Type

map : Std.PHashMap Lean.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 : Lean.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 : Lean.Name) :

Lean.MetaM Lean.Meta.Match.MatchEqns