def Lean.IO.FS.Stream.readUTF8 (h : IO.FS.Stream) (nBytes : Nat) : IO String

Equations

• Lean.IO.FS.Stream.readUTF8 h nBytes = do let bytes ← h.read (USize.ofNat nBytes) match String.fromUTF8? bytes with | some s => pure s | x => throw (IO.userError "invalid UTF-8")

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

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

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