TransformTotality.RequestedTranspose: type of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/transform_totality.bend as TransformTotality
Lines 132-146 of bendtorch-core@0.1.0.0/src/tensor/transform_totality.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/transform_totality.bend&start_line=132&end_line=146

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/tensor/core.bend as Core
import bendtorch-core@0.1.0.0/src/tensor/transforms.bend as Transforms
import bendtorch-core@0.1.0.0/src/tensor/axis_spec.bend as Axis
import bendtorch-core@0.1.0.0/src/tensor/transpose_spec.bend as Transpose

type RequestedTranspose<-input: Shape.Shape, -original: Core.Tensor<input>, -a: U32, -b: U32> is Data:
  RequestedTranspose{-plan: Layout.Plan<input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0)>,
    -retained: Core.Tensor<input>, -target: Core.Tensor<Layout.output(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan)>,
    -exact: {(retained, Done{Core.Packed{Layout.output(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan), target}}) ==
      Transforms.transpose_copy(input, original, a, b) : Core.Tensor<input> & Result<&2, &1, Transforms.Error, Core.Dynamic>},
    -dimensions: {Shape.dimensions(Layout.output(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan)) ==
      Axis.order(U32, Shape.dimensions(input), Shape.naturals(Transpose.requested_axes(Shape.rank_dimensions(Shape.dimensions(input)), U32.to_nat(a), U32.to_nat(b)))) : List<&2, U32>},
    -prefix: Transforms.Prefix<input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan, original, retained, target,
      Shape.logical_numel(Shape.dimensions(Layout.output(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan)))>,
    -mapping: @+index: U32 -> @mapping: Layout.Mapping<input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan, index> ->
      {Some{Layout.source_index(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan, index, mapping)} ==
        transpose_reference(input, Layout.output(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan), a, b, index) : Maybe<&2, U32>},
    -linear: @+index: U32 -> @-inside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(Layout.output(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan)))) == True{} : Bool} ->
      {Core.observe(Layout.output(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan), target, index) ==
        reference_observe(input, original, transpose_reference(input, Layout.output(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan), a, b, index)) : Maybe<&2, F32>}}

Uses (30):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=F32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe
  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=Pair
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Result
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma
  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/core.bend&name=Shape
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=dimensions
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=logical_numel
  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=rank_dimensions
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/axis_spec.bend&name=order
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=Dynamic
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=Tensor
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=observe
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/layout.bend&name=Mapping
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/layout.bend&name=Plan
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/layout.bend&name=output
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/layout.bend&name=source_index
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/layout.bend&name=transpose_axes
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/transform_totality.bend&name=reference_observe
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/transform_totality.bend&name=transpose_reference
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/transforms.bend&name=Error
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/transforms.bend&name=Prefix
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/transforms.bend&name=transpose_copy
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/transpose_spec.bend&name=requested_axes