Documentation

Lean.Elab.Quotation

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

      Transform sequence of pushes and appends into acceptable code

      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
            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.
              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
                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For

                        match #

                        In a single match step, we match the first discriminant against the "head" of the first pattern of the first alternative. This datatype describes what kind of check this involves, which helps other patterns decide if they are covered by the same check and don't have to be checked again (see also MatchResult).

                        • unconditional: Lean.Elab.Term.Quotation.HeadCheck

                          match step that always succeeds: _, x, `($x), ...

                        • shape: List Lean.SyntaxNodeKindOption NatLean.Elab.Term.Quotation.HeadCheck

                          match step based on kind and, optionally, arity of discriminant If arity is given, that number of new discriminants is introduced. covered patterns should then introduce the same number of new patterns. We actually check the arity at run time only in the case of null nodes since it should otherwise by implied by the node kind. without arity: `($x:k) with arity: any quotation without an antiquotation head pattern

                        • slice: NatNatLean.Elab.Term.Quotation.HeadCheck

                          Match step that succeeds on null nodes of arity at least numPrefix + numSuffix, introducing discriminants for the first numPrefix children, one null node for those in between, and for the numSuffix last children. example: ([$x, $xs,*, $y]) is slice 2 2`

                        • other: Lean.SyntaxLean.Elab.Term.Quotation.HeadCheck

                          other, complicated match step that will probably only cover identical patterns example: antiquotation splices `($[...]*)

                        Instances For

                          Describe whether a pattern is covered by a head check (induced by the pattern itself or a different pattern).

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

                            All necessary information on a pattern head.

                            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