Documentation

Lean.Parser.Module

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.

Instances For
    Instances For
      def Lean.Parser.testParseModule (env : Lean.Environment) (fname : String) (contents : String) :
      IO (Lean.TSyntax `Lean.Parser.Module.module)
      Instances For
        def Lean.Parser.testParseFile (env : Lean.Environment) (fname : Lake.FilePath) :
        IO (Lean.TSyntax `Lean.Parser.Module.module)
        Instances For