Documentation

Lean.Parser.Module

Equations
    Instances For
      Equations
        Instances For
          Equations
            Instances For
              Equations
                Instances For
                  Equations
                    Instances For
                      Equations
                        Instances For

                          Parser for a Lean module. We never actually run this parser but instead use the imperative definitions below that return the same syntax tree structure, but add error recovery. Still, it is helpful to have a Parser definition for it in order to auto-generate helpers such as the pretty printer.

                          Equations
                            Instances For
                              Equations
                                Instances For
                                  Instances For
                                    def Lean.Parser.parseHeader (inputCtx : InputContext) :
                                    IO (TSyntax `Lean.Parser.Module.header × ModuleParserState × MessageLog)
                                    Equations
                                      Instances For
                                        Equations
                                          Instances For
                                            Equations
                                              Instances For
                                                def Lean.Parser.testParseModule (env : Environment) (fname contents : String) :
                                                IO (TSyntax `Lean.Parser.Module.module)
                                                Equations
                                                  Instances For
                                                    def Lean.Parser.testParseFile (env : Environment) (fname : System.FilePath) :
                                                    IO (TSyntax `Lean.Parser.Module.module)
                                                    Equations
                                                      Instances For