Os.File
Part of Os.
handle File
An open file. Closed when this value dies, including on a panic, so a file opened in a scope needs no cleanup.
File.close is still offered and still returns a Result, because closing can fail: a buffered write is flushed by the close, and that is exactly when a full disk is discovered. Call it when that error matters; rely on the handle when it does not. Closing twice is harmless.
let File.read (f: File) (max_len: Int): Result[Bytes, String]
Up to max_len bytes. An empty result is END OF FILE, not a failure: the same three-way split Net.read_bytes makes, and for the same reason: a reader looping until the end needs to tell "nothing left" from "something broke".
let File.write (f: File) (data: Bytes): Result[Int, String]
len MUST be bound BEFORE .as_cstr() runs, the same ordering Net.write spells out: the pointer is an interior one into the cell, and reading .len() afterwards in the same argument list is how that bug was found on the wire the first time.
let File.seek (f: File) (offset: Int) (from: Seek): Result[Int, String]
The new absolute position.
let File.flush (f: File): Result[Unit, String]
Makes buffered writes visible without giving up the handle.
let File.close (f: File): Result[Unit, String]
Closing is OPTIONAL: the handle closes the file when it dies. Call this when a failed final flush is something the program should react to rather than lose. Calling it twice, or letting the handle run afterwards, is harmless.