source
structure Lean.Meta.Match.MatchEqns :
Type

- eqnNames : Array Name
- splitterName : Name
- splitterAltNumParams : Array Nat

Instances For

source
def Lean.Meta.Match.instInhabitedMatchEqns.default :
MatchEqns
Equations

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

Instances For

source
instance Lean.Meta.Match.instInhabitedMatchEqns :
Inhabited MatchEqns
Equations

- Lean.Meta.Match.instInhabitedMatchEqns = { default := Lean.Meta.Match.instInhabitedMatchEqns.default }

source
def Lean.Meta.Match.instReprMatchEqns.repr :
MatchEqns → Nat → Format
Equations

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

Instances For

source
instance Lean.Meta.Match.instReprMatchEqns :
Repr MatchEqns
Equations

- Lean.Meta.Match.instReprMatchEqns = { reprPrec := Lean.Meta.Match.instReprMatchEqns.repr }

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

- e.size = e.eqnNames.size

Instances For

source
structure Lean.Meta.Match.MatchEqnsExtState :
Type

- map : PHashMap Name MatchEqns
- eqns : PHashSet Name

Instances For

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

- Lean.Meta.Match.instInhabitedMatchEqnsExtState = { default := Lean.Meta.Match.instInhabitedMatchEqnsExtState.default }

source
def Lean.Meta.Match.instInhabitedMatchEqnsExtState.default :
MatchEqnsExtState
Equations

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

Instances For

source
opaque Lean.Meta.Match.matchEqnsExt :
EnvExtension MatchEqnsExtState
source
def Lean.Meta.Match.registerMatchEqns (matchDeclName : Name) (matchEqns : MatchEqns) :
CoreM Unit
Equations

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

Instances For

source
@[extern lean_get_match_equations_for]
opaque Lean.Meta.Match.getEquationsFor (matchDeclName : Name) :
MetaM MatchEqns
source
def Lean.Meta.Match.isMatchEqnTheorem (env : Environment) (declName : Name) :
Bool

Returns `true` if `declName` is the name of a `match` equational theorem.

Equations

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

Instances For