def read_checked_storage_keeps

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

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

278def read_checked_storage_keeps(+depth: Nat, +length: Nat, -array: Array<F32>, +index: U32,
279  -balanced: Model.Balanced(F32, depth, array), -valid: {Storage.bounds(depth, length) == True{} : Bool},
280  certificate: ReadCheckedKeeps<depth, length, array, index, Nat.is_lt(U32.to_nat(index), length), {==}, balanced, valid>) ->
281  StorageReadKeeps<Storage.Owned{depth, length, array, balanced, valid}, index>:
282  ReadCheckedKeeps{kept} = certificate
283  StorageReadKeeps{kept}