def permute_source_transposed

bendtorch-core@0.1.0.0 · src/tensor/transpose_PROOF.bend:254

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/tensor/observation.bend as Values

254def permute_source_transposed(+input: Shape.Shape, +rows: U32, +columns: U32,
255  +matrix: {Shape.dimensions(input) == [rows, columns] : List<&2, U32>}, +j: Nat,
256  +j_below: {Nat.is_lt(j, U32.to_nat(columns)) == True{} : Bool}, +l: Nat,
257  +l_below: {Nat.is_lt(l, U32.to_nat(rows)) == True{} : Bool}) ->
258  {Values.permute_source(input, [1, 0], U32.from_nat(Nat.add(Nat.mul(j, U32.to_nat(rows)), l))) ==
259    Some{U32.from_nat(Nat.add(Nat.mul(l, U32.to_nat(columns)), j))} : Maybe<&2, U32>}:
260  +index = U32.from_nat(Nat.add(Nat.mul(j, U32.to_nat(rows)), l))
261  %Equal.sym(List<&2, U32>, Shape.dimensions(input), [rows, columns], matrix) :
262    {transposed_source(_, index) == Some{U32.from_nat(Nat.add(Nat.mul(l, U32.to_nat(columns)), j))} : Maybe<&2, U32>}
263  matrix_source(rows, columns, j, l, j_below, l_below, transposed_index_exact(input, rows, columns, matrix, j, j_below, l, l_below))