~/jendhub

def index_of

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

import bendtorch-core@0.1.0.0/src/tensor/gather_LAWS.bend as GatherLAWS
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

188# A gather index is built as a tensor of its dimensions is: refused past
189# rank 4 or 2^20 elements with the shape's own error, else it holds the
190# shape of those dimensions.
191def index_of(+entries: List<&2, U32>, -dimensions: List<&2, U32>, built: Shape.ConstructResult<dimensions>) ->
192  Result<&2, &2, Gather.Error, Gather.Index>:
193  match built:
194    case Shape.SError{error}:
195      Fail{Gather.TensorError{Core.ShapeError{error}}}
196    case Shape.SBuilt{+shape, preserved}:
197      Done{Gather.Index{shape, entries}}

Uses (7)

Used by (2)