BackwardLAWS.unused_leaf_none: law of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/autograd/backward_LAWS.bend as BackwardLAWS
Lines 269-278 of bendtorch-core@0.1.0.0/src/autograd/backward_LAWS.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward_LAWS.bend&start_line=269&end_line=278

import Base
import bendtorch-core@0.1.0.0/src/autograd/backward.bend as Backward

# With x, y and z recorded and z only used by a node newer than the output
# x * y, backward of x * y seeds the output, leaves z and the newer node None,
# and gives x and y their VJP.
law unused_leaf_none:
  for +x: F32
  for +y: F32
  for +z: F32
  {slots_after(Backward.backward(program_unused(x, y, z), 3n)) ==
    Done{[None{}, Some{1.0}, None{}, Some{F32.mul(1.0, x)}, Some{F32.mul(1.0, y)}]} :
    Result<&2, &2, Backward.Error, List<&2, Maybe<&2, F32>>>}

Uses (9):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=F32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=F32.mul
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Result
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward.bend&name=Error
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward.bend&name=backward
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward_LAWS.bend&name=program_unused
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward_LAWS.bend&name=slots_after