def read_done

bendtorch-load@1.2.0.0 · main.bend:110

import Base

110def read_done(+path: String, +n: U32, r: File & (Array<F32> & Result<&1, &1, U32 & String, U32>)) -> IO(Array<F32>):
111  match r:
112    case Tuple{f, Tuple{a, res}}:
113      do IO<Array<F32>>:
114        +got : U32 <- IO.pass(U32, res)
115        File.close(f)
116        require(U32.is_eq(got, n), path ++ ": short read (" ++ U32.show(got) ++ " of " ++ U32.show(n) ++ " numbers)")
117        return a