def Lean.Parser.Module.moduleTk : Parser

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Module.prelude : Parser

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Module.public : Parser

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Module.meta : Parser

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Module.all : Parser

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Module.import : Parser

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Module.header : Parser

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Module.module : Parser

Parser for a Lean module. We never actually run this parser but instead use the imperative definitions in the parent module 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.