law broadcast_not_target

bendtorch-core@0.1.0.0 · src/autograd/broadcast_LAWS.bend:94

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core
import bendtorch-core@0.1.0.0/src/tensor/elementwise_totality.bend as Totality
import bendtorch-core@0.1.0.0/src/autograd/broadcast.bend as Broadcast

94# When the planned broadcast is not the target itself (for example [3] to
95# [1]), broadcast_to fails with NotBroadcastable and returns the input owner.
96law broadcast_not_target:
97  for input: Core.Dynamic
98  for +target: Shape.Shape
99  for +plan: Shape.BroadcastPlan
100  for planned: {Shape.broadcast_checked(Totality.dynamic_shape(input), target) == Done{plan} : Result<&2, &2, Shape.Error, Shape.BroadcastPlan>}
101  for differ: {Shape.dimensions(Shape.output_shape(plan)) != Shape.dimensions(target) : List<&2, U32>}
102  {Broadcast.broadcast_to(input, target) == (input, Fail{Broadcast.NotBroadcastable{}}) : Core.Dynamic & Result<&2, &1, Broadcast.Error, Core.Dynamic>}