BendtorchLoad.read_done: def of bendtorch-load@1.3.0.0
Import: import bendtorch-load@1.3.0.0/main.bend as BendtorchLoad
Lines 112-119 of bendtorch-load@1.3.0.0/main.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-load@1.3.0.0/main.bend&start_line=112&end_line=119

import Base

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

Uses (18):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=F32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=File
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=File.close
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=IO
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=IO.bind
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=IO.pass
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=IO.pure
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Result
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=String
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=String.append
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.is_eq
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.show
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Unit
  https://jend.leeeet.dev/definition.txt?path=bendtorch-load@1.3.0.0/main.bend&name=require