def decoded_word_fits

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

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

140def decoded_word_fits(+shape: Shape.Shape, +index: U32,
141  +inside: {True{} == Nat.is_lt(U32.to_nat(index), Shape.elements(shape)) : Bool}) ->
142  Coordinates.Fits(Shape.extents(shape), Shape.naturals(Shape.words(Shape.digits(Shape.extents(shape), U32.to_nat(index))))):
143  %Equal.sym(List<&2, Nat>, Shape.naturals(Shape.words(Shape.digits(Shape.extents(shape), U32.to_nat(index)))),
144    Shape.digits(Shape.extents(shape), U32.to_nat(index)),
145    WordConversion.naturals_words_fitting(Shape.dimensions(shape), Shape.digits(Shape.extents(shape), U32.to_nat(index)), decoded_fit(shape, index, inside))) :
146      Coordinates.Fits(Shape.extents(shape), _)
147  Coordinates.fits_of(Shape.extents(shape), Shape.digits(Shape.extents(shape), U32.to_nat(index)), decoded_fit(shape, index, inside))