def transpose_decided_model

bendtorch-core@0.1.0.0 · src/tensor/transform_PROOF.bend:1057

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/transform_LAWS.bend as Laws
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/transpose_spec.bend as TransposeSpec

1057def transpose_decided_model(+input: Shape.Shape, source: Core.Tensor<input>, +a: U32, +b: U32,
1058  decision: Shape.BoolCase<TransposeSpec.valid(input, a, b)>) ->
1059  Transforms.PublicModel<input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), source,
1060    Transforms.transpose_decided(input, source, a, b, decision)>:
1061  match decision:
1062    case Shape.BFalse{equal}:
1063      Transforms.PublicModel{Unit{}}
1064    case Shape.BTrue{equal}:
1065      Laws.permute_result_interpretation(input, source, Layout.transpose_axes(Shape.dimensions(input), a, b, 0))