def planned_output_dimensions
bendtorch-core@0.1.0.0 · src/tensor/elementwise_PROOF.bend:519
import bendtorch-core@0.1.0.0/src/tensor/elementwise_PROOF.bend as ElementwisePROOF
import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/shape/unique_proofs.bend as Unique
519def planned_output_dimensions(+left: Shape.Shape, +right: Shape.Shape, +plan: Shape.BroadcastPlan, +output: List<&2, U32>,
520 +alignment: Shape.Broadcast<Shape.extents(left), Shape.extents(right), Shape.naturals(output)>,
521 +sources: {(Shape.dimensions(Shape.left_shape(plan)), Shape.dimensions(Shape.right_shape(plan))) ==
522 (Shape.dimensions(left), Shape.dimensions(right)) : List<&2, U32> & List<&2, U32>}) ->
523 {Shape.dimensions(Shape.output_shape(plan)) == output : List<&2, U32>}:
524 natural_dimensions_equal(Shape.dimensions(Shape.output_shape(plan)), output,
525 Unique.broadcast_unique(Shape.extents(left), Shape.extents(right), Shape.extents(Shape.output_shape(plan)), Shape.naturals(output),
526 %Equal.cong(List<&2, U32> & List<&2, U32>, List<&2, Nat>, pair => Shape.naturals(Pair.fst(List<&2, U32>, List<&2, U32>, pair)),
527 (Shape.dimensions(Shape.left_shape(plan)), Shape.dimensions(Shape.right_shape(plan))), (Shape.dimensions(left), Shape.dimensions(right)), sources) :
528 Shape.Broadcast<_, Shape.extents(right), Shape.extents(Shape.output_shape(plan))>
529 %Equal.cong(List<&2, U32> & List<&2, U32>, List<&2, Nat>, pair => Shape.naturals(Pair.snd(List<&2, U32>, List<&2, U32>, pair)),
530 (Shape.dimensions(Shape.left_shape(plan)), Shape.dimensions(Shape.right_shape(plan))), (Shape.dimensions(left), Shape.dimensions(right)), sources) :
531 Shape.Broadcast<Shape.extents(Shape.left_shape(plan)), _, Shape.extents(Shape.output_shape(plan))>
532 Shape.alignment(plan), alignment))