def inverse_words_roundtrip

bendtorch-core@0.1.0.0 · src/tensor/permutation_mapping.bend:610

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

610def inverse_words_roundtrip(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan<input, axes>, +coordinate: Layout.CheckedCoordinate<Layout.output(input, axes, plan)>,
611  +values: List<&2, U32>, inverse: {Some{values} == Layout.inverse_coordinates(Shape.dimensions(input), axes, Layout.coordinate_values(Layout.output(input, axes, plan), coordinate), 0) : Maybe<&2, List<&2, U32>>}) ->
612  {True{} == Layout.maybe_same(Layout.reorder(values, axes), Some{Layout.coordinate_values(Layout.output(input, axes, plan), coordinate)}) : Bool}:
613  %Equal.sym(Maybe<&2, List<&2, U32>>, Layout.reorder(values, axes), Some{Layout.coordinate_values(Layout.output(input, axes, plan), coordinate)},
614    inverse_words_reordered(input, axes, plan, coordinate, values, inverse)) :
615      {True{} == Layout.maybe_same(_, Some{Layout.coordinate_values(Layout.output(input, axes, plan), coordinate)}) : Bool}
616  Equal.sym(Bool, Layout.words_same(Layout.coordinate_values(Layout.output(input, axes, plan), coordinate), Layout.coordinate_values(Layout.output(input, axes, plan), coordinate)), True{},
617    words_same_refl(Layout.coordinate_values(Layout.output(input, axes, plan), coordinate)))