# Documentation

Lean.Elab.ParseImportsFast

Instances For
Equations
Equations
@[inline]
Equations
• = { imports := s.imports, pos := pos, error? := s.error? }
@[inline]
Equations
• = { imports := s.imports, pos := s.pos, error? := some msg }
Equations
@[inline]
Equations
@[inline]
Equations
Equations
@[specialize #[]]
@[inline]
Equations
@[inline]
Equations
Equations
@[inline]
Equations
@[inline]
Equations
• One or more equations did not get rendered due to their size.
@[inline]
Equations
• One or more equations did not get rendered due to their size.
Equations
@[inline]
Equations
@[inline]
Equations
@[inline]
Equations
Equations
• One or more equations did not get rendered due to their size.
def Lean.parseImports' (input : String) (fileName : String) :

Simpler and faster version of parseImports. We use it to implement Lake.

Equations
• One or more equations did not get rendered due to their size.
• imports? :
• errors :
Instances For
Equations
• imports :
Instances For
Equations
@[export lean_print_imports_json]
def Lean.printImportsJson (fileNames : ) :
Equations
• One or more equations did not get rendered due to their size.