def attach_length

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

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/storage/main.bend as Storage
import bendtorch-core@0.1.0.0/src/tensor/lifecycle.bend as Lifecycle

70def attach_length(+shape: Shape.Shape, -original: Storage.Storage, pair: Storage.Storage & Nat,
71  -same: {pair == Storage.length(original) : Storage.Storage & Nat}) ->
72  Result<&2, &1, Error, Tensor<shape>>:
73  (storage, +n) = pair
74  attach_decided(shape, storage, n,
75    %Equal.sym(Storage.Storage & Nat, (storage, n), Storage.length(original), same) :
76      {Lifecycle.length_owner(_) == Lifecycle.length_value(_) : Nat}
77    Lifecycle.length_exact(original),
78    Shape.bool_case(Nat.is_eq(n, Shape.elements(shape))))