BendMlAutograd.reverse_eq_forward: law of bend-ml-autograd@0.1.1.0
Import: import bend-ml-autograd@0.1.1.0/main.bend as BendMlAutograd
Lines 110-116 of bend-ml-autograd@0.1.1.0/main.bend: https://jend.leeeet.dev/read.txt?path=bend-ml-autograd@0.1.1.0/main.bend&start_line=110&end_line=116

import Base

# LAW (reverse_eq_forward): for any expression made of constants, X, sums
# and products, the reverse-mode gradient (starting with gradient 1 at the output)
# equals the forward-mode derivative. It holds for every x.
law reverse_eq_forward:
  for +e: NE
  for +x: Nat
  {nbwd(e, x, 1n) == nfwd(e, x) : Nat}

Uses (8):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul
  https://jend.leeeet.dev/definition.txt?path=bend-ml-autograd@0.1.1.0/main.bend&name=NE
  https://jend.leeeet.dev/definition.txt?path=bend-ml-autograd@0.1.1.0/main.bend&name=nbwd
  https://jend.leeeet.dev/definition.txt?path=bend-ml-autograd@0.1.1.0/main.bend&name=nbwd_ok
  https://jend.leeeet.dev/definition.txt?path=bend-ml-autograd@0.1.1.0/main.bend&name=nfwd
  https://jend.leeeet.dev/definition.txt?path=bend-ml-nat-lemmas@0.1.2.0/main.bend&name=mul_one_l