def fitted_not_reducible

bendtorch-core@0.1.0.0 · src/autograd/reduce_PROOF.bend:661

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/reduce.bend as Reduce

661def fitted_not_reducible(input: Core.Dynamic, +target: Shape.Shape, +plan: Shape.BroadcastPlan, +dims: List<&2, U32>, flag: Bool,
662  decided: {flag == Layout.words_same(Shape.dimensions(Shape.output_shape(plan)), dims) : Bool},
663  differ: {Shape.dimensions(Shape.output_shape(plan)) != dims : List<&2, U32>}) ->
664  {Reduce.fitted(input, target, plan, flag) == (input, Fail{Reduce.NotReducible{}}) :
665    Core.Dynamic & Result<&2, &1, Reduce.Error, Core.Dynamic>}:
666  match flag:
667    case False{}:
668      {==}
669    case True{}:
670      Empty.absurd({Reduce.fitted(input, target, plan, True{}) == (input, Fail{Reduce.NotReducible{}}) :
671        Core.Dynamic & Result<&2, &1, Reduce.Error, Core.Dynamic>},
672        differ(TransformProof.words_equal(Shape.dimensions(Shape.output_shape(plan)), dims, decided)))