def tensor_done

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

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith
import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core
import bendtorch-core@0.1.0.0/src/tensor/allocation_spec.bend as Allocation

86def tensor_done(+shape: Shape.Shape, result: Result<&2, &1, Core.Error, Core.Tensor<shape>>,
87  exact: {Allocation.tensor_length(shape, result) == Some{Shape.logical_numel(Shape.dimensions(shape))} : Maybe<&2, Nat>}) -> Allocation.TensorDone<shape, result>:
88  match result:
89    case Fail{error}:
90      Empty.absurd(Allocation.TensorDone<shape, Fail{error}>,
91        Arith.clash(Equal.cong(Maybe<&2, Nat>, Bool, value => Maybe.is_some(&2, Nat, value), None{}, Some{Shape.logical_numel(Shape.dimensions(shape))}, exact)))
92    case Done{tensor}:
93      Allocation.TensorDone{tensor, {==}}