PermuteValuesContractLAWS.permute_contract: law of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/permute_values_contract_LAWS.bend as PermuteValuesContractLAWS
Lines 12-22 of bendtorch-core@0.1.0.0/src/tensor/permute_values_contract_LAWS.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/permute_values_contract_LAWS.bend&start_line=12&end_line=22

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/permute_values_records.bend as Records
import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core

# `permute_copy` of a `Core.from_values(input, values)` tensor by a valid
# permutation succeeds with dimensions `Axis.order(dims, axes)`; output index i
# holds `values[permute_source(input, axes, i)]`, and the returned source
# still holds `values[j]` at every j.
law permute_contract:
  for +input: Shape.Shape
  for +values: List<&2, F32>
  for counted: {List.length(&2, F32, values) == Shape.logical_numel(Shape.dimensions(input)) : Nat}
  for +axes: List<&2, U32>
  for valid: {True{} == Layout.bijective(input, axes) : Bool}
  Records.PermuteContract<input, values, axes>

Uses (12):
  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.length
  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=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/layout.bend&name=bijective
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/permute_values.bend&name=permute_contract
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/permute_values_records.bend&name=PermuteContract