def left_count

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

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

213def left_count(+left: Shape.Shape, +right: Shape.Shape, +plan: Shape.BroadcastPlan,
214  +planned: {Shape.broadcast_checked(left, right) == Done{plan} : Result<&2, &2, Shape.Error, Shape.BroadcastPlan>}) ->
215  {U32.to_nat(Shape.count(left)) == Shape.logical_numel(Shape.dimensions(Shape.left_shape(plan))) : Nat}:
216  Equal.trans(Nat, U32.to_nat(Shape.count(left)), Shape.logical_numel(Shape.dimensions(left)), Shape.logical_numel(Shape.dimensions(Shape.left_shape(plan))), Reads.count_exact(left),
217    Equal.cong(List<&2, U32>, Nat, dims => Shape.logical_numel(dims), Shape.dimensions(left), Shape.dimensions(Shape.left_shape(plan)),
218      Equal.sym(List<&2, U32>, Shape.dimensions(Shape.left_shape(plan)), Shape.dimensions(left), left_dims(left, right, plan, planned))))