Documentation

Lean.Elab.Match

Remark: if the discriminat is Systax.missing, we abort the elaboration of the match-expression. 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

match

into

let d := ; match

Recall that Syntax.setArg stx i arg is a no-op when i is out-of-bounds.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    Instances For
      Equations
      Instances For
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For

            We convert the collected PatternVars intro PatternVarDecl

            Instances For

              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 n. Moreover, nil and 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 _s 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.

              Auxiliary structure for storing an type mismatch exception when processing the pattern #idx of some alternative.

              Instances For
                • 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.

                • explicitPatternVars : Array Lean.FVarId

                  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 normalize procedure.

                Instances For

                  Return true iff e is an explicit pattern variable provided by the user.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For

                    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). Recall that mkLambdaFVars now allows us to abstract both free variables and metavariables.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        Instances For

                          The Bool context is true iff we are inside of an "inaccessible" pattern.

                          Main method for withDepElimPatterns.

                          • 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.
                          • k is the continuation that is executed in an updated local context with the all pattern variables (explicit and implicit). Note that, patternVarDecls are all replaced since they may depend on implicit pattern variables (i.e., metavariables) that are converted into new free variables by this method.
                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              Instances For
                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For
                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For
                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For