def length_exact

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

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

111def length_exact(storage: Storage.Storage) ->
112  {length_owner(Storage.length(storage)) == length_value(Storage.length(storage)) : Nat}:
113  match storage:
114    case Storage.Empty{}:
115      {==}
116    case Storage.Owned{d, n, array, balanced, valid}:
117      {==}