def count_same

bendtorch-core@0.1.0.0 · src/tensor/permute_values.bend:131

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_build_proof.bend as PermuteProof
import bendtorch-core@0.1.0.0/src/tensor/read_contract.bend as Reads

131# The output count of a permute is its input count.
132def count_same(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan<input, axes>) -> {U32.to_nat(Shape.count(Layout.output(input, axes, plan))) == U32.to_nat(Shape.count(input)) : Nat}:
133  Equal.trans(Nat, U32.to_nat(Shape.count(Layout.output(input, axes, plan))), Shape.logical_numel(Shape.dimensions(Layout.output(input, axes, plan))), U32.to_nat(Shape.count(input)), Reads.count_exact(Layout.output(input, axes, plan)),
134    Equal.trans(Nat, Shape.logical_numel(Shape.dimensions(Layout.output(input, axes, plan))), Shape.logical_numel(Shape.dimensions(input)), U32.to_nat(Shape.count(input)), PermuteProof.plan_numel(input, axes, plan), Equal.sym(Nat, U32.to_nat(Shape.count(input)), Shape.logical_numel(Shape.dimensions(input)), Reads.count_exact(input))))