law transpose_contract

bendtorch-core@0.1.0.0 · src/tensor/permute_values_contract_LAWS.bend:24

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/tensor/transpose_spec.bend as Transpose
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

24# `transpose_copy(a, b)` of a `Core.from_values` tensor with both axes in
25# range is the permute contract with the axes that swap a and b.
26law transpose_contract:
27  for +input: Shape.Shape
28  for +values: List<&2, F32>
29  for counted: {List.length(&2, F32, values) == Shape.logical_numel(Shape.dimensions(input)) : Nat}
30  for +a: U32
31  for +b: U32
32  for inside: {True{} == Transpose.valid(input, a, b) : Bool}
33  Records.TransposeContract<input, values, a, b>