Documentation

Lean.Parser.Extra

The parser optional(p), or (p)?, parses p if it succeeds, otherwise it succeeds with no value.

Note that because ? is a legal identifier character, one must write (p)? or p ? for it to parse correctly. ident? will not work; one must write (ident)? instead.

This parser has arity 1: it produces a nullKind node containing either zero arguments (for the none case) or the list of arguments produced by p. (In particular, if p has arity 0 then the two cases are not differentiated!)

Equations
Instances For

    The parser many(p), or p*, repeats p until it fails, and returns the list of results.

    The argument p is "auto-grouped", meaning that if the arity is greater than 1 it will be automatically replaced by group(p) to ensure that it produces exactly 1 value.

    This parser has arity 1: it produces a nullKind node containing one argument for each invocation of p (or group(p)).

    Equations
    Instances For

      The parser many1(p), or p+, repeats p until it fails, and returns the list of results. p must succeed at least once, or this parser will fail.

      Note that this parser produces the same parse tree as the many(p) / p* combinator, and one matches both p* and p+ using $[ .. ]* syntax in a syntax match. (There is no $[ .. ]+ syntax.)

      The argument p is "auto-grouped", meaning that if the arity is greater than 1 it will be automatically replaced by group(p) to ensure that it produces exactly 1 value.

      This parser has arity 1: it produces a nullKind node containing one argument for each invocation of p (or group(p)).

      Equations
      Instances For

        The parser ident parses a single identifier, possibly with namespaces, such as foo or bar.baz. The identifier must not be a declared token, so for example it will not match "def" because def is a keyword token. Tokens are implicitly declared by using them in string literals in parser declarations, so syntax foo := "bla" will make bla no longer legal as an identifier.

        Identifiers can contain special characters or keywords if they are escaped using the «» characters: «def» is an identifier named def, and «x» is treated the same as x. This is useful for using disallowed characters in identifiers such as «foo.bar».baz or «hello world».

        This parser has arity 1: it produces a Syntax.ident node containing the parsed identifier. You can use TSyntax.getId to extract the name from the resulting syntax object.

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

            The parser hygieneInfo parses no text, but captures the current macro scope information as though it parsed an identifier at the current position. It returns a hygieneInfoKind node around an .ident which is Name.anonymous but with macro scopes like a regular identifier.

            This is used to implement have := ... syntax: the hygieneInfo between the have and := substitutes for the identifier which would normally go there as in have x :=, so that we can expand have := to have this := while retaining the usual macro name resolution behavior. See doc/macro_overview.md for more information about macro hygiene.

            This parser has arity 1: it produces a Syntax.ident node containing the parsed identifier. You can use TSyntax.getHygieneInfo to extract the name from the resulting syntax object.

            Equations
            Instances For

              The parser num parses a numeric literal in several bases:

              • Decimal: 129
              • Hexadecimal: 0xdeadbeef
              • Octal: 0o755
              • Binary: 0b1101

              This parser has arity 1: it produces a numLitKind node containing an atom with the text of the literal. You can use TSyntax.getNat to extract the number from the resulting syntax object.

              Equations
              Instances For

                The parser scientific parses a scientific-notation literal, such as 1.3e-24.

                This parser has arity 1: it produces a scientificLitKind node containing an atom with the text of the literal. You can use TSyntax.getScientific to extract the parts from the resulting syntax object.

                Equations
                Instances For

                  The parser str parses a string literal, such as "foo" or "\r\n". Strings can contain C-style escapes like \n, \", \x00 or \u2665, as well as literal unicode characters like . Newlines in a string are interpreted literally.

                  This parser has arity 1: it produces a strLitKind node containing an atom with the raw literal (including the quote marks and without interpreting the escapes). You can use TSyntax.getString to decode the string from the resulting syntax object.

                  Equations
                  Instances For

                    The parser char parses a character literal, such as 'a' or '\n'. Character literals can contain C-style escapes like \n, \", \x00 or \u2665, as well as literal unicode characters like , but must evaluate to a single unicode codepoint, so '♥' is allowed but '❤️' is not (since it is two codepoints but one grapheme cluster).

                    This parser has arity 1: it produces a charLitKind node containing an atom with the raw literal (including the quote marks and without interpreting the escapes). You can use TSyntax.getChar to decode the string from the resulting syntax object.

                    Equations
                    Instances For

                      The parser name parses a name literal like `foo. The syntax is the same as for identifiers (see ident) but with a leading backquote.

                      This parser has arity 1: it produces a nameLitKind node containing the raw literal (including the backquote). You can use TSyntax.getName to extract the name from the resulting syntax object.

                      Equations
                      Instances For
                        @[inline]

                        The parser group(p) parses the same thing as p, but it wraps the results in a groupKind node.

                        This parser always has arity 1, even if p does not. Parsers like p* are automatically rewritten to group(p)* if p does not have arity 1, so that the results from separate invocations of p can be differentiated.

                        Equations
                        Instances For
                          @[inline]

                          The parser many1Indent(p) is equivalent to withPosition((colGe p)+). This has the effect of parsing one or more occurrences of p, where each subsequent p parse needs to be indented the same or more than the first parse.

                          This parser has arity 1, and returns a list of the results from p. p is "auto-grouped" if it is not arity 1.

                          Equations
                          Instances For
                            @[inline]

                            The parser manyIndent(p) is equivalent to withPosition((colGe p)*). This has the effect of parsing zero or more occurrences of p, where each subsequent p parse needs to be indented the same or more than the first parse.

                            This parser has arity 1, and returns a list of the results from p. p is "auto-grouped" if it is not arity 1.

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

                                    No-op parser combinator that annotates subtrees to be ignored in syntax patterns.

                                    Equations
                                    Instances For
                                      @[inline]

                                      No-op parser that advises the pretty printer to emit a non-breaking space.

                                      Equations
                                      Instances For
                                        @[inline]

                                        No-op parser that advises the pretty printer to emit a space/soft line break.

                                        Equations
                                        Instances For
                                          @[inline]

                                          No-op parser that advises the pretty printer to emit a hard line break.

                                          Equations
                                          Instances For
                                            @[inline]

                                            No-op parser combinator that advises the pretty printer to emit a Format.fill node.

                                            Equations
                                            Instances For
                                              @[inline]

                                              No-op parser combinator that advises the pretty printer to emit a Format.group node.

                                              Equations
                                              Instances For
                                                @[inline]

                                                No-op parser combinator that advises the pretty printer to indent the given syntax without grouping it.

                                                Equations
                                                Instances For
                                                  @[inline]

                                                  No-op parser combinator that advises the pretty printer to group and indent the given syntax. By default, only syntax categories are grouped.

                                                  Equations
                                                  Instances For
                                                    @[inline]

                                                    No-op parser combinator that advises the pretty printer to dedent the given syntax. Dedenting can in particular be used to counteract automatic indentation.

                                                    Equations
                                                    Instances For
                                                      @[inline]

                                                      No-op parser combinator that allows the pretty printer to omit the group and indent operation in the enclosing category parser.

                                                      syntax ppAllowUngrouped "by " tacticSeq : term
                                                      -- allows a `by` after `:=` without linebreak in between:
                                                      theorem foo : True := by
                                                        trivial
                                                      
                                                      Equations
                                                      Instances For
                                                        @[inline]

                                                        No-op parser combinator that advises the pretty printer to dedent the given syntax, if it was grouped by the category parser. Dedenting can in particular be used to counteract automatic indentation.

                                                        Equations
                                                        Instances For
                                                          @[inline]

                                                          No-op parser combinator that prints a line break. The line break is soft if the combinator is followed by an ungrouped parser (see ppAllowUngrouped), otherwise hard.

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