def read_done

bendtorch-load@1.3.0.0 · main.bend:112

import Base

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