def right_count

bendtorch-core@0.1.0.0 · src/tensor/contracts/binary_proofs.bend:220

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/tensor/read_contract.bend as Reads

220def right_count(+left: Shape.Shape, +right: Shape.Shape, +plan: Shape.BroadcastPlan,
221  +planned: {Shape.broadcast_checked(left, right) == Done{plan} : Result<&2, &2, Shape.Error, Shape.BroadcastPlan>}) ->
222  {U32.to_nat(Shape.count(right)) == Shape.logical_numel(Shape.dimensions(Shape.right_shape(plan))) : Nat}:
223  Equal.trans(Nat, U32.to_nat(Shape.count(right)), Shape.logical_numel(Shape.dimensions(right)), Shape.logical_numel(Shape.dimensions(Shape.right_shape(plan))), Reads.count_exact(right),
224    Equal.cong(List<&2, U32>, Nat, dims => Shape.logical_numel(dims), Shape.dimensions(right), Shape.dimensions(Shape.right_shape(plan)),
225      Equal.sym(List<&2, U32>, Shape.dimensions(Shape.right_shape(plan)), Shape.dimensions(right), right_dims(left, right, plan, planned))))