~/jendhub

def right_dims

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

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

205def right_dims(+left: Shape.Shape, +right: Shape.Shape, +plan: Shape.BroadcastPlan,
206  +planned: {Shape.broadcast_checked(left, right) == Done{plan} : Result<&2, &2, Shape.Error, Shape.BroadcastPlan>}) ->
207  {Shape.dimensions(Shape.right_shape(plan)) == Shape.dimensions(right) : List<&2, U32>}:
208  Equal.cong(List<&2, U32> & List<&2, U32>, List<&2, U32>, p => Pair.snd(List<&2, U32>, List<&2, U32>, p),
209    (Shape.dimensions(Shape.left_shape(plan)), Shape.dimensions(Shape.right_shape(plan))), (Shape.dimensions(left), Shape.dimensions(right)),
210    %planned : {ShapeLaws.planned_dimensions(left, right, _) == (Shape.dimensions(left), Shape.dimensions(right)) : List<&2, U32> & List<&2, U32>}
211    PlanProof.broadcast_checked_plan(left, right))

Uses (16)

Used by (1)