BackwardLAWS.backward_mul: law of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/autograd/backward_LAWS.bend as BackwardLAWS
Lines 234-239 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=234&end_line=239

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

law backward_mul:
  for +x: F32
  for +y: F32
  {observe(program_binary(Backward.Times{}, x, y), 2n) ==
    (Done{F32.mul(x, y)}, Done{[Some{1.0}, Some{F32.mul(1.0, x)}, Some{F32.mul(1.0, y)}]}) :
    Result<&2, &2, Backward.Error, F32> & Result<&2, &2, Backward.Error, List<&2, Maybe<&2, F32>>>}

Uses (11):
  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=Pair
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Result
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward.bend&name=Binary
  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_LAWS.bend&name=observe
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward_LAWS.bend&name=program_binary