def kept_as_sum

bendtorch-core@0.1.0.0 · src/autograd/sum_dims_PROOF.bend:97

import Base
import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core
import bendtorch-core@0.1.0.0/src/autograd/reduce.bend as Reduce
import bendtorch-core@0.1.0.0/src/autograd/sum_dims.bend as SumDims
import bendtorch-core@0.1.0.0/src/autograd/sum_dims_LAWS.bend as Laws

97# With keepdim, summed only renames reduce_to's error.
98def kept_as_sum(+dropped: List<&2, U32>, pair: Core.Dynamic & Result<&2, &1, Reduce.Error, Core.Dynamic>) ->
99  {SumDims.summed(dropped, True{}, pair) == Laws.as_sum(pair) : Core.Dynamic & Result<&2, &1, SumDims.Error, Core.Dynamic>}:
100  match pair:
101    case Tuple{input, Fail{error}}:
102      {==}
103    case Tuple{input, Done{output}}:
104      {==}