def Lean.Lsp.ResolvableCompletionList.compressFast (l : ResolvableCompletionList) : String

Fast path for (toJson l).compress that skips the intermediate Json object. Used in place of (toJson l).compress in the language server.

Equations

• l.compressFast = Lean.Lsp.ResolvableCompletionList.compressItemsFast✝ ("{\"isIncomplete\":" ++ toString l.isIncomplete ++ ",\"items\":[") l.items 0 ++ "]}"