ReluLAWS.scalar_relu_backward_zeroed: law of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/relu_LAWS.bend as ReluLAWS
Lines 88-96 of bendtorch-core@0.1.0.0/src/tensor/relu_LAWS.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/relu_LAWS.bend&start_line=88&end_line=96

import Base
import bendtorch-core@0.1.0.0/src/tensor/elementwise.bend as Elementwise

# ReluBackward is PyTorch's relu gradient, threshold_backward(g, relu(x), 0),
# with x on the left and g on the right: +0.0 where x is at most zero, so the
# gradient at +0.0 and -0.0 is +0.0, and g's own word otherwise, NaN x
# included.
law scalar_relu_backward_zeroed:
  for +left: F32
  for +right: F32
  for zeroed: {Elementwise.at_most_zero(left) == True{} : Bool}
  {Elementwise.scalar(Elementwise.ReluBackward{}, left, right) == 0.0 : F32}

Uses (7):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=F32
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise.bend&name=Operation
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise.bend&name=at_most_zero
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise.bend&name=scalar
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise.bend&name=zero_if