Documentation

Lean.Elab.Syntax

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

Instances For
    Instances For
      @[inline, reducible]
      Instances For
        @[inline, reducible]
        Instances For

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

          Instances For

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

            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.

              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[_,]

                Instances For

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

                  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.

                    Instances For