Documentation

Lean.Parser.Module

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

              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
              • 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
                  Instances For
                    def Lean.Parser.parseHeader (inputCtx : InputContext) :
                    IO (TSyntax `Lean.Parser.Module.header × ModuleParserState × MessageLog)
                    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
                          Equations
                          Instances For
                            def Lean.Parser.testParseModule (env : Environment) (fname contents : String) :
                            IO (TSyntax `Lean.Parser.Module.module)
                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              def Lean.Parser.testParseFile (env : Environment) (fname : System.FilePath) :
                              IO (TSyntax `Lean.Parser.Module.module)
                              Equations
                              Instances For