Documentation

Lean.Meta.Match.MatchEqsExt

structure Lean.Meta.Match.MatchEqns :

eqnNames : Array Lake.Name
splitterName : Lake.Name
splitterAltNumParams : Array Nat

Instances For

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) :

Equations

e.size = e.eqnNames.size

Instances For

structure Lean.Meta.Match.MatchEqnsExtState :

map : Lean.PHashMap Lake.Name Lean.Meta.Match.MatchEqns

Instances For

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.

Instances For

@[extern lean_get_match_equations_for]

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

Lean.MetaM Lean.Meta.Match.MatchEqns