def IO.FS.Stream.readJson (h : IO.FS.Stream) (nBytes : Nat) : IO Lean.Json

Consumes nBytes bytes from the stream, interprets the bytes as a utf-8 string and the string as a valid JSON object.

Equations

• IO.FS.Stream.readJson h nBytes = do let bytes ← h.read (USize.ofNat nBytes) let s : String := String.fromUTF8Unchecked bytes IO.ofExcept (Lean.Json.parse s)

def IO.FS.Stream.writeJson (h : IO.FS.Stream) (j : Lean.Json) : IO Unit

Equations

• IO.FS.Stream.writeJson h j = do h.putStr (Lean.Json.compress j) h.flush