law backward_unknown

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

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

379# backward of an output the tape does not hold is refused with UnknownNode.
380law backward_unknown:
381  for +entries: List<&2, Backward.Entry>
382  for +output: Nat
383  for outside: {Nat.is_lt(output, List.length(&2, Backward.Entry, entries)) == False{} : Bool}
384  {Backward.backward(Backward.Tape{entries}, output) == Fail{Backward.UnknownNode{}} : Result<&2, &2, Backward.Error, Backward.Tape>}