Remark: if the discriminat is
Systax.missing, we abort the elaboration of the
This can happen due to error recovery. Example
example : (p ∨ p) → p := fun h => match
If we don't abort, the elaborator loops because we will keep trying to expand
let d :=
Syntax.setArg stx i arg is a no-op when
i is out-of-bounds.
- matchType : Lean.Expr
- isDep : Bool
truewhen performing dependent elimination. We use this to decide whether we optimize the "match unit" case. See
Remark: when performing dependent pattern matching, we often had to write code such as
def Vec.map' (f : α → β) (xs : Vec α n) : Vec β n :=
match n, xs with
| _, nil => nil
| _, cons a as => cons (f a) (map' f as)
We had to include
n and the
_s because the type of
xs depends on
cons a as have different types.
This was quite tedious. So, we have implemented an automatic "discriminant refinement procedure".
The procedure is based on the observation that we get a type error whenenver we forget to include
and the indices a discriminant depends on. So, we catch the exception, check whether the type of the discriminant
is an indexed family, and add their indices as new discriminants.
The current implementation, adds indices as they are found, and does not try to "sort" the new discriminants.
If the refinement process fails, we report the original error message.
- userName : Lake.Name
When visiting an assigned metavariable, if it has an user-name. We save it here. We want to preserve these user-names when generating new pattern variables.
Pattern variables that were explicitly provided by the user. Recall that implicit parameters and
_are elaborated as metavariables, and then converted into pattern variables by the
Return true iff
e is an explicit pattern variable provided by the user.
Normalize the pattern and collect all patterns variables (explicit and implicit).
This method is the one that decides where the inaccessible annotations must be inserted.
The pattern variables are both free variables (for explicit pattern variables) and metavariables (for implicit ones).
mkLambdaFVars now allows us to abstract both free variables and metavariables.
Main method for
PatternVarDecls: are the explicit pattern variables provided by the user.
ps: are the patterns provided by the user.
matchType: the expected typ for this branch. It depends on the explicit pattern variables and the implicit ones that are still represented as metavariables, and are found by this function.
kis the continuation that is executed in an updated local context with the all pattern variables (explicit and implicit). Note that,
patternVarDeclsare all replaced since they may depend on implicit pattern variables (i.e., metavariables) that are converted into new free variables by this method.