BackwardLAWS.vjp_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 201-210 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=201&end_line=210

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

# d(a*b)/da = b and d(a*b)/db = a, with the operand values saved at record
# time: the first operand receives g * right, the second g * left.
law vjp_mul:
  for +a: Nat
  for +b: Nat
  for +left: F32
  for +right: F32
  for +g: F32
  {Backward.vjp(Backward.Mul{a, b, left, right}, g) ==
    [Backward.Contribution{a, F32.mul(g, right)}, Backward.Contribution{b, F32.mul(g, left)}] : List<&2, Backward.Contribution>}

Uses (7):
  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=Nat
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward.bend&name=Contribution
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward.bend&name=Node
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward.bend&name=vjp