def broadcast_checked_plan
bendtorch-core@0.1.0.0 · src/shape/plan_proofs.bend:23
import bendtorch-core@0.1.0.0/src/shape/plan_proofs.bend as PlanProofs
import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/shape/LAWS.bend as Laws
23def broadcast_checked_plan(+left: Shape.Shape, +right: Shape.Shape) -> {Laws.planned_dimensions(left, right, Shape.broadcast_checked(left, right)) == (Shape.dimensions(left), Shape.dimensions(right)) : List<&2, U32> & List<&2, U32>}:
24 +left_rank = Shape.rank_dimensions(Shape.dimensions(left))
25 +right_rank = Shape.rank_dimensions(Shape.dimensions(right))
26 plan_align(left, right, Nat.sub(right_rank, left_rank), Nat.sub(left_rank, right_rank), Shape.minimal(left_rank, right_rank), Shape.align(Shape.pad_words(Nat.sub(right_rank, left_rank), Shape.dimensions(left)), Shape.pad_words(Nat.sub(left_rank, right_rank), Shape.dimensions(right))))