some hif the discriminant is annotated withh:
Instances For
- numParams : Nat
- numDiscrs : Nat
- discrInfos : Array Lean.Meta.Match.DiscrInfo
discrInfos[i] = { hName? := some h }if the i-th discriminant was annotated withh :.
A "matcher" auxiliary declaration has the following structure:
numParamsparameters- motive
numDiscrsdiscriminators (aka major premises)altNumParams.sizealternatives (aka minor premises) where alternativeihasaltNumParams[i]parametersuElimPos?issome poswhen the matcher can eliminate in different universe levels, andposis the position of the universe level parameter that specifies the elimination universe. It isnoneif the matcher only eliminates intoProp.
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
- name : Lake.Name
- info : Lean.Meta.MatcherInfo
Instances For
Instances For
def
Lean.Meta.Match.Extension.addMatcherInfo
(env : Lean.Environment)
(matcherName : Lake.Name)
(info : Lean.Meta.MatcherInfo)
:
Instances For
Instances For
Instances For
Instances For
def
Lean.Meta.getMatcherInfo?
{m : Type → Type}
[Monad m]
[Lean.MonadEnv m]
(declName : Lake.Name)
:
Instances For
@[export lean_is_matcher]
Instances For
def
Lean.Meta.isMatcher
{m : Type → Type}
[Monad m]
[Lean.MonadEnv m]
(declName : Lake.Name)
:
m Bool