def output

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

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core
import bendtorch-core@0.1.0.0/src/tensor/gather.bend as Gather

73# ... and its output, the input's dimensions with that length at the axis,
74# or the refusal of the shape's own checks (rank and capacity).
75def output(-dimensions: List<&2, U32>, +plan: Gather.Plan, built: Shape.ConstructResult<dimensions>) ->
76  Result<&2, &2, Gather.Error, Gather.Planned>:
77  match built:
78    case Shape.SError{error}:
79      Fail{Gather.TensorError{Core.ShapeError{error}}}
80    case Shape.SBuilt{+shape, preserved}:
81      Done{Gather.Planned{plan, shape}}