def finish_read_length

bendtorch-core@0.1.0.0 · src/tensor/lifecycle.bend:22

import Base
import bendtorch-core@0.1.0.0/src/storage/main.bend as Storage
import bendtorch-core@0.1.0.0/src/storage/model.bend as Model

22def finish_read_length(+d: Nat, +n: Nat, -original: Array<F32>, +i: U32,
23  result: Array<F32> & F32, -exact: {result == Array.get(F32, original, i) : Array<F32> & F32},
24  -balanced: Model.Balanced(F32, d, original), -valid: {Storage.bounds(d, n) == True{} : Bool}) ->
25  {retained_read(Storage.finish_read(d, n, original, i, result, exact, balanced, valid)) == n : Nat}:
26  (array, value) = result
27  {==}