PermuteValues.count_same: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/permute_values.bend as PermuteValues
Lines 131-134 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=131&end_line=134

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

# The output count of a permute is its input count.
def 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}:
  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)),
    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))))

Uses (14):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  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/tensor/layout.bend&name=Plan
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/layout.bend&name=output
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/permute_build_proof.bend&name=plan_numel
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/read_contract.bend&name=count_exact