def clone_first_length

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

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

87def clone_first_length(storage: Storage.Storage) ->
88  {first_length(Storage.clone(storage)) == logical_length(storage) : Nat}:
89  match storage:
90    case Storage.Empty{}:
91      {==}
92    case Storage.Owned{+d, +n, array, balanced, valid}:
93      finish_clone_first(d, n, array, Array.clone(F32, array), {==}, balanced, valid)