some h
if the discriminant is annotated withh:
Instances For
A "matcher" auxiliary declaration has the following structure:
numParams
parameters- motive
numDiscrs
discriminators (aka major premises)altNumParams.size
alternatives (aka minor premises) where alternativei
hasaltNumParams[i]
parametersuElimPos?
issome pos
when the matcher can eliminate in different universe levels, andpos
is the position of the universe level parameter that specifies the elimination universe. It isnone
if the matcher only eliminates intoProp
.
- numParams : Nat
- numDiscrs : Nat
discrInfos[i] = { hName? := some h }
if the i-th discriminant was annotated withh :
.
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
def
Lean.Meta.Match.Extension.addMatcherInfo
(env : Environment)
(matcherName : Name)
(info : MatcherInfo)
:
Equations
Instances For
Equations
Instances For
def
Lean.Meta.Match.addMatcherInfo
{m : Type → Type}
[Monad m]
[MonadEnv m]
(matcherName : Name)
(info : MatcherInfo)
:
m Unit
Equations
Instances For
Equations
Instances For
def
Lean.Meta.getMatcherInfo?
{m : Type → Type}
[Monad m]
[MonadEnv m]
(declName : Name)
:
m (Option MatcherInfo)
Equations
Instances For
@[export lean_is_matcher]