BendMlBinaryRead.read_bf16_at: def of bend-ml-binary-read@0.2.0.0
Import: import bend-ml-binary-read@0.2.0.0/main.bend as BendMlBinaryRead
Lines 45-52 of bend-ml-binary-read@0.2.0.0/main.bend: https://jend.leeeet.dev/read.txt?path=bend-ml-binary-read@0.2.0.0/main.bend&start_line=45&end_line=52

import Base

# n little-endian BF16 numbers (2 * n bytes) at the byte offset hi * 2^32 + lo, each widened exactly into a cell of
# `a`: the F32 whose top 16 bits are the BF16's and whose low 16 bits are zero (what bf16.to(torch.float32) gives).
# Stops at a's capacity and at the end of the file, answers the number of whole numbers read, and leaves the cells
# past them as they were (a last odd byte is dropped). The file's position does not move.
def read_bf16_at(file: File, hi: U32, lo: U32, n: U32, a: Array<F32>) ->
  IO(File & (Array<F32> & Result<&1, &1, U32 & String, U32>)):
  import "./read_at.c"
  import "./read_at.js"

Uses (8):
  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=IO
  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=String
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32