~/jendhub

def decoded_fit

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

import bendtorch-core@0.1.0.0/src/tensor/permutation_mapping.bend as PermutationMapping
import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/shape/coordinate_proofs.bend as Coordinates

134def decoded_fit(+shape: Shape.Shape, +index: U32,
135  +inside: {True{} == Nat.is_lt(U32.to_nat(index), Shape.elements(shape)) : Bool}) ->
136  {True{} == Shape.fit(Shape.extents(shape), Shape.digits(Shape.extents(shape), U32.to_nat(index))) : Bool}:
137  %decoded_indices(shape, index, inside) : {True{} == Shape.fit(Shape.extents(shape), _) : Bool}
138  Coordinates.fit_indices(Shape.extents(shape), decoded_coordinate(shape, index, inside))

Uses (12)

Used by (2)