Streaming JSON writer that avoids stack overflow on large values.

partial def writeJsonTo (h : IO.FS.Handle) : Lean.Json → IO Unit

Write a Lean.Json value to a file handle without building an intermediate string.

def writeJsonFile (path : String) (json : Lean.Json) : IO Unit

Write a Lean.Json value to a file, ensuring the handle is flushed even on exception.

Equations

• writeJsonFile path json = do let h ← IO.FS.Handle.mk { toString := path } IO.FS.Mode.write tryFinally (writeJsonTo h json) h.flush