def length_preserved

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

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

119def length_preserved(storage: Storage.Storage) ->
120  {length_owner(Storage.length(storage)) == logical_length(storage) : Nat}:
121  match storage:
122    case Storage.Empty{}:
123      {==}
124    case Storage.Owned{d, n, array, balanced, valid}:
125      {==}