Documentation

Lean.Data.Json.Stream

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

Equations

IO.FS.Stream.readJson h nBytes = do let bytes ← IO.FS.Stream.read h (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) :

Equations

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