def get_length

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

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

39def get_length(storage: Storage.Storage, +i: U32) ->
40  {retained_read(Storage.get(storage, i)) == logical_length(storage) : Nat}:
41  match storage:
42    case Storage.Empty{}:
43      {==}
44    case Storage.Owned{+d, +n, array, balanced, valid}:
45      get_checked_length(d, n, array, i, Nat.is_lt(U32.to_nat(i), n), {==}, balanced, valid)