Documentation

Lean.Elab.PatternVar

@[reducible, inline]
Equations
Instances For

    Patterns define new local variables. This module collect them and preprocess _ occurring in patterns. Recall that an _ may represent anonymous variables or inaccessible terms that are implied by typing constraints. Thus, we represent them with fresh named holes ?x. After we elaborate the pattern, if the metavariable remains unassigned, we transform it into a regular pattern variable. Otherwise, it becomes an inaccessible term.

    Macros occurring in patterns are expanded before the collectPatternVars method is executed. The following kinds of Syntax are handled by this module

    State for the pattern variable collector monad.

    Instances For

      An application in a pattern can be

      1- A constructor application The elaborator assumes fields are accessible and inductive parameters are not accessible.

      2- A regular application (f ...) where f is tagged with [match_pattern]. The elaborator assumes implicit arguments are not accessible and explicit ones are accessible.

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

        Check whether stx is a pattern variable or constructor-like (i.e., constructor or constant tagged with [match_pattern] attribute)

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

          Collect pattern variables occurring in the match-alternative object views. It also returns the updated views.

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

            Return the pattern variables in the given pattern. Remark: this method is not used by the main match elaborator, but in the precheck hook and other macros (e.g., at Do.lean).

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

              Return the pattern variables occurring in the given patterns. This method is used in the match and do notation elaborators

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