~/jendhub

def left_dims

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

import bendtorch-core@0.1.0.0/src/tensor/contracts/binary_proofs.bend as BinaryProofs
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 ShapeLaws
import bendtorch-core@0.1.0.0/src/shape/plan_proofs.bend as PlanProof

196# The plan's input shapes have the inputs' dimensions.
197def left_dims(+left: Shape.Shape, +right: Shape.Shape, +plan: Shape.BroadcastPlan,
198  +planned: {Shape.broadcast_checked(left, right) == Done{plan} : Result<&2, &2, Shape.Error, Shape.BroadcastPlan>}) ->
199  {Shape.dimensions(Shape.left_shape(plan)) == Shape.dimensions(left) : List<&2, U32>}:
200  Equal.cong(List<&2, U32> & List<&2, U32>, List<&2, U32>, p => Pair.fst(List<&2, U32>, List<&2, U32>, p),
201    (Shape.dimensions(Shape.left_shape(plan)), Shape.dimensions(Shape.right_shape(plan))), (Shape.dimensions(left), Shape.dimensions(right)),
202    %planned : {ShapeLaws.planned_dimensions(left, right, _) == (Shape.dimensions(left), Shape.dimensions(right)) : List<&2, U32> & List<&2, U32>}
203    PlanProof.broadcast_checked_plan(left, right))

Uses (16)

Used by (1)