def read_checked_storage

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

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

221def read_checked_storage(+depth: Nat, +length: Nat, -array: Array<F32>, +index: U32,
222  -balanced: Model.Balanced(F32, depth, array), -valid: {Storage.bounds(depth, length) == True{} : Bool},
223  certificate: ReadCheckedModel<depth, length, array, index, Nat.is_lt(U32.to_nat(index), length), {==}, balanced, valid>) ->
224  StorageReadModel<Storage.Owned{depth, length, array, balanced, valid}, index>:
225  ReadCheckedModel{meaning} = certificate
226  StorageReadModel{meaning}