law reduce_empty_zeros

bendtorch-core@0.1.0.0 · src/autograd/reduce_LAWS.bend:144

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

144# Reducing an empty contribution gives zeros at every target position, not an
145# empty tensor: for example [0, 3] reduced to [1, 3] is three zeros.
146law reduce_empty_zeros:
147  for input: Core.Dynamic
148  for +target: Shape.Shape
149  for empty: {Shape.logical_numel(Totality.dimensions(input)) == 0n : Nat}
150  Zeros<target, Reduce.reduce_to(input, target)>