PermutationMapping.codec_decoded: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/permutation_mapping.bend as PermutationMapping
Lines 45-59 of bendtorch-core@0.1.0.0/src/tensor/permutation_mapping.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/permutation_mapping.bend&start_line=45&end_line=59

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

def codec_decoded(+dimensions: List<&2, U32>, +index: U32) ->
  {Layout.reverse_words(Layout.unflatten_words(Layout.reverse_words(dimensions), index)) ==
    Shape.words(Shape.digits(Shape.naturals(dimensions), U32.to_nat(index))) : List<&2, U32>}:
  Equal.trans(List<&2, U32>, Layout.reverse_words(Layout.unflatten_words(Layout.reverse_words(dimensions), index)),
    Shape.words(Shape.digits_words(dimensions, U32.to_nat(index))),
    Shape.words(Shape.digits(Shape.naturals(dimensions), U32.to_nat(index))),
    Equal.trans(List<&2, U32>, Layout.reverse_words(Layout.unflatten_words(Layout.reverse_words(dimensions), index)),
      Layout.reverse_words(Layout.reverse_words(Shape.words(Shape.digits_words(dimensions, U32.to_nat(index))))),
      Shape.words(Shape.digits_words(dimensions, U32.to_nat(index))),
      Equal.cong(List<&2, U32>, List<&2, U32>, dims =>
        Layout.reverse_words(Layout.reverse_words(Shape.words(Shape.digits_words(dims, U32.to_nat(index))))),
        Layout.reverse_words(Layout.reverse_words(dimensions)), dimensions, reverse_involution(dimensions)),
      reverse_involution(Shape.words(Shape.digits_words(dimensions, U32.to_nat(index))))),
    Equal.cong(List<&2, Nat>, List<&2, U32>, Shape.words, Shape.digits_words(dimensions, U32.to_nat(index)),
      Shape.digits(Shape.naturals(dimensions), U32.to_nat(index)), Coordinates.digits_words_spec(dimensions, U32.to_nat(index))))

Uses (14):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.to_nat
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/coordinate_proofs.bend&name=digits_words_spec
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=digits
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=digits_words
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=naturals
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=words
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/layout.bend&name=reverse_words
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/layout.bend&name=unflatten_words
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/permutation_mapping.bend&name=reverse_involution