Documentation

Lean.Parser.Module

source
def Lean.Parser.Module.prelude:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Module.import:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Module.header:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Module.module:
Lean.Parser.Parser

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.
source
def Lean.Parser.Module.updateTokens (c : Lean.Parser.ParserContext) :
Lean.Parser.ParserContext
Equations
  • One or more equations did not get rendered due to their size.
source
structure Lean.Parser.ModuleParserState:
Type
source
instance Lean.Parser.instInhabitedModuleParserState:
Inhabited Lean.Parser.ModuleParserState
Equations
source
def Lean.Parser.parseHeader (inputCtx : Lean.Parser.InputContext) :
IO (Lean.Syntax × Lean.Parser.ModuleParserState × Lean.MessageLog)
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.isEOI (s : Lean.Syntax) :
Bool
Equations
source
def Lean.Parser.isExitCommand (s : Lean.Syntax) :
Bool
Equations
source
def Lean.Parser.topLevelCommandParserFn:
Lean.Parser.ParserFn
Equations
source
def Lean.Parser.parseCommand (inputCtx : Lean.Parser.InputContext) (pmctx : Lean.Parser.ParserModuleContext) (mps : Lean.Parser.ModuleParserState) (messages : Lean.MessageLog) :
Lean.Syntax × Lean.Parser.ModuleParserState × Lean.MessageLog
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.testParseModuleAux (env : Lean.Environment) (inputCtx : Lean.Parser.InputContext) (s : Lean.Parser.ModuleParserState) (msgs : Lean.MessageLog) (stxs : Array Lean.Syntax) :
IO (Array Lean.Syntax)
Equations
source
partial def Lean.Parser.testParseModuleAux.parse (env : Lean.Environment) (inputCtx : Lean.Parser.InputContext) (state : Lean.Parser.ModuleParserState) (msgs : Lean.MessageLog) (stxs : Array Lean.Syntax) :
IO (Array Lean.Syntax)
source
def Lean.Parser.testParseModule (env : Lean.Environment) (fname : String) (contents : String) :
IO Lean.Syntax
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.testParseFile (env : Lean.Environment) (fname : System.FilePath) :
IO Lean.Syntax
Equations