def sized_done

mlbend-datasets@0.1.6.0 · main.bend:232

import mlbend-datasets@0.1.6.0/main.bend as MlbendDatasets
import Base

232def sized_done(pair: File & Result<&1, &1, U32 & String, U32>) -> IO(Maybe<&1, String>):
233  (file, result) = pair
234  match result:
235    case Fail{e}:
236      do IO<Maybe<&1, String>>:
237        File.close(file)
238        return None{}
239    case Done{size}:
240      do IO<Maybe<&1, String>>:
241        pair : File & Result<&1, &1, U32 & String, String> <- File.read(file, size)
242        m : Maybe<&1, String> <- read_done(pair)
243        return m

Uses (14)

Used by (1)