PermutationMapping.decoded_indices: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/permutation_mapping.bend as PermutationMapping
Lines 118-132 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=118&end_line=132

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

def decoded_indices(+shape: Shape.Shape, +index: U32,
  +inside: {True{} == Nat.is_lt(U32.to_nat(index), Shape.elements(shape)) : Bool}) ->
  {Shape.indices(Shape.extents(shape), decoded_coordinate(shape, index, inside)) ==
    Shape.digits(Shape.extents(shape), U32.to_nat(index)) : List<&2, Nat>}:
  Equal.trans(List<&2, Nat>, Shape.indices(Shape.extents(shape), decoded_coordinate(shape, index, inside)),
    Shape.digits(Shape.extents(shape), Shape.Fin.value(Shape.numel(Shape.extents(shape)),
      Coordinates.fin_from(Shape.numel(Shape.extents(shape)), U32.to_nat(index), Coordinates.size_fits(shape, U32.to_nat(index), inside)))),
    Shape.digits(Shape.extents(shape), U32.to_nat(index)),
    Coordinates.digits_unflatten(Shape.extents(shape),
      Coordinates.fin_from(Shape.numel(Shape.extents(shape)), U32.to_nat(index), Coordinates.size_fits(shape, U32.to_nat(index), inside))),
    Equal.cong(Nat, List<&2, Nat>, value => Shape.digits(Shape.extents(shape), value),
      Shape.Fin.value(Shape.numel(Shape.extents(shape)),
        Coordinates.fin_from(Shape.numel(Shape.extents(shape)), U32.to_nat(index), Coordinates.size_fits(shape, U32.to_nat(index), inside))),
      U32.to_nat(index), Coordinates.fin_from_value(Shape.numel(Shape.extents(shape)), U32.to_nat(index),
        Coordinates.size_fits(shape, U32.to_nat(index), inside))))

Uses (20):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  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=Nat.is_lt
  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_unflatten
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/coordinate_proofs.bend&name=fin_from
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/coordinate_proofs.bend&name=fin_from_value
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/coordinate_proofs.bend&name=size_fits
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Fin.value
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Shape
  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=elements
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=extents
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=indices
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=numel
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/permutation_mapping.bend&name=decoded_coordinate