law backward_success

bendtorch-core@0.1.0.0 · src/autograd/backward_LAWS.bend:422

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

422# Otherwise backward accumulates the gradients of pass into the slots.
423law backward_success:
424  for +entries: List<&2, Backward.Entry>
425  for +output: Nat
426  for inside: {Nat.is_lt(output, List.length(&2, Backward.Entry, entries)) == True{} : Bool}
427  for sound: {Backward.wired(Backward.nodes(entries), List.length(&2, Backward.Entry, entries)) == True{} : Bool}
428  {Backward.backward(Backward.Tape{entries}, output) ==
429    Done{Backward.Tape{Backward.merge(entries, Backward.pass(Backward.nodes(entries), List.length(&2, Backward.Entry, entries), output))}} :
430    Result<&2, &2, Backward.Error, Backward.Tape>}