def read_go

bendtorch-load@1.3.0.0 · main.bend:121

import Base
import bend-ml-binary-read@0.2.0.0/main.bend as R
import bendtorch@1.3.0.0/main.bend as T

121def read_go(+path: String, +n: U32, f: File, +size: W64) -> IO(Array<F32>):
122  do IO<Array<F32>>:
123    require(W64.eq(size, W64.mul_small(W64.of(n), 4)), path ++ ": expected " ++ W64.show(W64.mul_small(W64.of(n), 4)) ++ " bytes, got " ++ W64.show(size))
124    rr : File & (Array<F32> & Result<&1, &1, U32 & String, U32>) <- R.read_f32_at(f, 0, 0, n, Array.new(F32, T.depth(U32.to_nat(n)), 0.0))
125    read_done(path, n, rr)