def codec_decoded

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

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

45def codec_decoded(+dimensions: List<&2, U32>, +index: U32) ->
46  {Layout.reverse_words(Layout.unflatten_words(Layout.reverse_words(dimensions), index)) ==
47    Shape.words(Shape.digits(Shape.naturals(dimensions), U32.to_nat(index))) : List<&2, U32>}:
48  Equal.trans(List<&2, U32>, Layout.reverse_words(Layout.unflatten_words(Layout.reverse_words(dimensions), index)),
49    Shape.words(Shape.digits_words(dimensions, U32.to_nat(index))),
50    Shape.words(Shape.digits(Shape.naturals(dimensions), U32.to_nat(index))),
51    Equal.trans(List<&2, U32>, Layout.reverse_words(Layout.unflatten_words(Layout.reverse_words(dimensions), index)),
52      Layout.reverse_words(Layout.reverse_words(Shape.words(Shape.digits_words(dimensions, U32.to_nat(index))))),
53      Shape.words(Shape.digits_words(dimensions, U32.to_nat(index))),
54      Equal.cong(List<&2, U32>, List<&2, U32>, dims =>
55        Layout.reverse_words(Layout.reverse_words(Shape.words(Shape.digits_words(dims, U32.to_nat(index))))),
56        Layout.reverse_words(Layout.reverse_words(dimensions)), dimensions, reverse_involution(dimensions)),
57      reverse_involution(Shape.words(Shape.digits_words(dimensions, U32.to_nat(index))))),
58    Equal.cong(List<&2, Nat>, List<&2, U32>, Shape.words, Shape.digits_words(dimensions, U32.to_nat(index)),
59      Shape.digits(Shape.naturals(dimensions), U32.to_nat(index)), Coordinates.digits_words_spec(dimensions, U32.to_nat(index))))