def fitted_not_target

bendtorch-core@0.1.0.0 · src/autograd/broadcast_PROOF.bend:309

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/layout.bend as Layout
import bendtorch-core@0.1.0.0/src/tensor/transform_PROOF.bend as TransformProof
import bendtorch-core@0.1.0.0/src/autograd/broadcast.bend as Broadcast

309def fitted_not_target(input: Core.Dynamic, +target: Shape.Shape, +plan: Shape.BroadcastPlan, flag: Bool,
310  decided: {flag == Layout.words_same(Shape.dimensions(Shape.output_shape(plan)), Shape.dimensions(target)) : Bool},
311  differ: {Shape.dimensions(Shape.output_shape(plan)) != Shape.dimensions(target) : List<&2, U32>}) ->
312  {Broadcast.fitted(input, target, plan, flag) == (input, Fail{Broadcast.NotBroadcastable{}}) :
313    Core.Dynamic & Result<&2, &1, Broadcast.Error, Core.Dynamic>}:
314  match flag:
315    case False{}:
316      {==}
317    case True{}:
318      Empty.absurd({Broadcast.fitted(input, target, plan, True{}) == (input, Fail{Broadcast.NotBroadcastable{}}) :
319        Core.Dynamic & Result<&2, &1, Broadcast.Error, Core.Dynamic>},
320        differ(TransformProof.words_equal(Shape.dimensions(Shape.output_shape(plan)), Shape.dimensions(target), decided)))