Documentation

Lean.Elab.Syntax

Expand optional «precedence» where «precedence» := leading_parser " : " >> precedenceParser

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

        (Try to) add a term info for the category catName at ref.

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

          (Try to) add a term info for the alias with info info at ref.

          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

                  Given a stx of category syntax, return a (newStx, lhsPrec?), where newStx is of category term. After elaboration, newStx should have type TrailingParserDescr if lhsPrec?.isSome, and ParserDescr otherwise.

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

                              Auxiliary function for creating declaration names from parser descriptions. Example: Given

                              syntax term "+" term : term
                              syntax "[" sepBy(term, ", ") "]"  : term
                              

                              It generates the names term_+_ and term[_,]

                              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

                                    Add macro scope to name if it does not already have them, and attrKind is local.

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

                                              Infer syntax kind k from first pattern, put alternatives of same kind into new macro/elab_rules (kind := k) via mkCmd (some k), leave remaining alternatives (via mkCmd none) to be recursively expanded.

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