Documentation

Lean.Elab.ParseImportsFast

Instances For
    @[specialize #[]]
    @[inline]
    Instances For
      @[inline]
      Instances For
        def Lean.parseImports' (input : String) (fileName : String) :

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

        Instances For
          Instances For
            @[export lean_print_imports_json]
            Instances For