PermuteValues.transpose_contract: def of bendtorch-core@0.1.0.0 Import: import bendtorch-core@0.1.0.0/src/tensor/permute_values.bend as PermuteValues Lines 462-505 of bendtorch-core@0.1.0.0/src/tensor/permute_values.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/permute_values.bend&start_line=462&end_line=505 import Base import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape 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 import bendtorch-core@0.1.0.0/src/tensor/from_values_contract.bend as FromValues import bendtorch-core@0.1.0.0/src/tensor/observation.bend as Values import bendtorch-core@0.1.0.0/src/tensor/transform_observation.bend as Observation import bendtorch-core@0.1.0.0/src/tensor/permute_values_records.bend as Records def transpose_contract(+input: Shape.Shape, +values: List<&2, F32>, counted: {List.length(&2, F32, values) == Shape.logical_numel(Shape.dimensions(input)) : Nat}, +a: U32, +b: U32, inside: {True{} == Transpose.valid(input, a, b) : Bool}) -> Records.TransposeContract: +counted = counted +inside = inside +axes = requested(input, a, b) +valid = requested_valid(input, a, b, inside) Records.TransposeContract{ FromValues.from_values_lift(input, values, counted, result => {Observation.failure_code(input, Observation.Transpose{a, b}, result) == Some{0} : Maybe<&2, U32>}, fits => transpose_lift(input, values, a, b, inside, fits, pair => {Some{Observation.failure_code_pair(input, pair)} == Some{0} : Maybe<&2, U32>}, permuted_code(input, values, axes, valid, fits))), FromValues.from_values_lift(input, values, counted, result => {Observation.applied_dimensions(input, Observation.Transpose{a, b}, result) == Some{Axis.order(U32, Shape.dimensions(input), Shape.naturals(axes))} : Maybe<&2, List<&2, U32>>}, fits => transpose_lift(input, values, a, b, inside, fits, pair => {Observation.applied_dimensions_pair(input, pair) == Some{Axis.order(U32, Shape.dimensions(input), Shape.naturals(axes))} : Maybe<&2, List<&2, U32>>}, permuted_dimensions(input, values, axes, valid, fits))), FromValues.from_values_lift(input, values, counted, result => {Observation.applied_length(input, Observation.Transpose{a, b}, result) == Some{Shape.logical_numel(Shape.dimensions(input))} : Maybe<&2, Nat>}, fits => transpose_lift(input, values, a, b, inside, fits, pair => {Observation.applied_length_pair(input, pair) == Some{Shape.logical_numel(Shape.dimensions(input))} : Maybe<&2, Nat>}, permuted_length(input, values, axes, valid, fits))), FromValues.from_values_lift(input, values, counted, result => {Observation.applied_count(input, Observation.Transpose{a, b}, result) == Some{Shape.count(input)} : Maybe<&2, U32>}, fits => transpose_lift(input, values, a, b, inside, fits, pair => {Observation.applied_count_pair(input, pair) == Some{Shape.count(input)} : Maybe<&2, U32>}, permuted_count(input, values, axes, valid, fits))), index => below => +below = below FromValues.from_values_lift(input, values, counted, result => {Observation.applied_value(input, Observation.Transpose{a, b}, index, result) == Values.listed(values, Values.permute_source(input, axes, index)) : Maybe<&2, F32>}, fits => transpose_lift(input, values, a, b, inside, fits, pair => {Observation.applied_value_pair(input, index, pair) == Values.listed(values, Values.permute_source(input, axes, index)) : Maybe<&2, F32>}, permuted_value(input, values, counted, axes, valid, index, below, fits))), other => below => +below = below FromValues.from_values_lift(input, values, counted, result => {Observation.kept_value(input, Observation.Transpose{a, b}, other, result) == List.get(&2, F32, values, U32.to_nat(other)) : Maybe<&2, F32>}, fits => transpose_lift(input, values, a, b, inside, fits, pair => {Observation.kept_value_pair(input, other, pair) == List.get(&2, F32, values, U32.to_nat(other)) : Maybe<&2, F32>}, permuted_kept(input, values, counted, axes, valid, other, below, fits)))} Uses (42): 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=List.get https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.length https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat 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=count 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/tensor/axis_spec.bend&name=order https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/from_values_contract.bend&name=from_values_lift https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/observation.bend&name=listed https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/observation.bend&name=permute_source https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/permute_values.bend&name=permuted_code https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/permute_values.bend&name=permuted_count https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/permute_values.bend&name=permuted_dimensions https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/permute_values.bend&name=permuted_kept https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/permute_values.bend&name=permuted_length https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/permute_values.bend&name=permuted_value https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/permute_values.bend&name=requested https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/permute_values.bend&name=requested_valid https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/permute_values.bend&name=transpose_lift https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/permute_values_records.bend&name=TransposeContract https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/transform_observation.bend&name=Request https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/transform_observation.bend&name=applied_count https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/transform_observation.bend&name=applied_count_pair https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/transform_observation.bend&name=applied_dimensions https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/transform_observation.bend&name=applied_dimensions_pair https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/transform_observation.bend&name=applied_length https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/transform_observation.bend&name=applied_length_pair https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/transform_observation.bend&name=applied_value https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/transform_observation.bend&name=applied_value_pair https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/transform_observation.bend&name=failure_code https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/transform_observation.bend&name=failure_code_pair https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/transform_observation.bend&name=kept_value https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/transform_observation.bend&name=kept_value_pair https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/transpose_spec.bend&name=valid