Documentation

Lean.Parser.Types

@[inline, reducible]
Instances For
    @[inline, reducible]
    Instances For
      def Lean.Parser.getNext (input : String) (pos : String.Pos) :

      Return character after position pos

      Instances For

        Maximal (and function application) precedence. In the standard lean language, no parser has precedence higher than maxPrec.

        Note that nothing prevents users from using a higher precedence, but we strongly discourage them from doing it.

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

                    Input string and related data. Recall that the FileMap is a helper structure for mapping String.Pos in the input string to line/column information.

                    Instances For

                      Input context derived from elaboration of previous commands.

                      Instances For

                        Parser context parts that can be updated without invalidating the parser cache.

                        Instances For

                          Parser context updateable in adaptUncacheableContextFn.

                          Instances For

                              Opaque parser context updateable using adaptCacheableContextFn and adaptUncacheableContextFn.

                              Instances For
                                Instances For
                                  Instances For
                                    Instances For
                                      Instances For

                                        A syntax array with an inaccessible prefix, used for sound caching.

                                        Instances For
                                          Instances For

                                            Reports given 'expected' messages at range of top stack element (assumed to be a single token). Replaces the element with missing and resets position to the token position. iniPos can be specified to avoid this position lookup but still must be identical to the token position.

                                            Instances For

                                              Reports given 'expected' message at range of top stack element (assumed to be a single token). Replaces the element with missing and resets position to the token position. iniPos can be specified to avoid this position lookup but still must be identical to the token position.

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

                                                  Create a simple parser combinator that inherits the info of the nested parser.

                                                  Instances For

                                                    Run p with a fresh cache, restore outer cache afterwards. p may access the entire syntax stack.

                                                    Instances For

                                                      Run p with a fresh cache, restore outer cache afterwards. p may access the entire syntax stack.

                                                      Instances For

                                                        Run p under the given context transformation with a fresh cache (see also withResetCacheFn).

                                                        Instances For

                                                          Run p and record result in parser cache for any further invocation with this parserName, parser context, and parser state. p cannot access syntax stack elements pushed before the invocation in order to make caching independent of parser history. As this excludes trailing parsers from being cached, we also reset lhsPrec, which is not read but set by leading parsers, to 0 in order to increase cache hits. Finally, errorMsg is also reset to none as a leading parser should not be called in the first place if there was an error.

                                                          Instances For

                                                            Run p and record result in parser cache for any further invocation with this parserName, parser context, and parser state. p cannot access syntax stack elements pushed before the invocation in order to make caching independent of parser history. As this excludes trailing parsers from being cached, we also reset lhsPrec, which is not read but set by leading parsers, to 0 in order to increase cache hits. Finally, errorMsg is also reset to none as a leading parser should not be called in the first place if there was an error.

                                                            Instances For