TransformPROOF.permuted_output: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/transform_PROOF.bend as TransformPROOF
Lines 1003-1020 of bendtorch-core@0.1.0.0/src/tensor/transform_PROOF.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/transform_PROOF.bend&start_line=1003&end_line=1020

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

def permuted_output(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan<input, axes>,
  -original: Core.Tensor<input>, -source: Core.Tensor<input>, -target: Core.Tensor<Layout.output(input, axes, plan)>,
  prefix: Transforms.Prefix<input, axes, plan, original, source, target,
    Shape.logical_numel(Shape.dimensions(Layout.output(input, axes, plan)))>) ->
  Transforms.PermuteOutput<input, axes, original, source, Core.Packed{Layout.output(input, axes, plan), target}>:
  Transforms.Prefix{kept, words, checked, written} = prefix
  Transforms.PermuteOutput{plan, {==}, kept, words, checked, written,
    other => bound => Equal.trans(Maybe<&2, F32>, Core.observe(Layout.output(input, axes, plan), target, U32.from_nat(other)),
      Core.checked_observe(Layout.output(input, axes, plan), target, U32.from_nat(other)),
      Transforms.expected_output(input, axes, plan, original, U32.from_nat(other)),
      {\{ObserveBridge: equal => Equal.sym(Maybe<&2, F32>,
        Core.checked_observe(Layout.output(input, axes, plan), target, U32.from_nat(other)),
        Core.observe(Layout.output(input, axes, plan), target, U32.from_nat(other)), equal)} :
          ObserveBridge<Layout.output(input, axes, plan), target, U32.from_nat(other)> ->
            {Core.observe(Layout.output(input, axes, plan), target, U32.from_nat(other)) ==
              Core.checked_observe(Layout.output(input, axes, plan), target, U32.from_nat(other)) : Maybe<&2, F32>}}(
                observe_bridge(Layout.output(input, axes, plan), target, U32.from_nat(other), checked(other, bound))),
      written(other, bound))}

Uses (21):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  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=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.from_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/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=checked_observe
  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=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/transform_PROOF.bend&name=ObserveBridge
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/transform_PROOF.bend&name=observe_bridge
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/transforms.bend&name=PermuteOutput
  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=expected_output