law record_unknown_right

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

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

363law record_unknown_right:
364  for +entries: List<&2, Backward.Entry>
365  for kind: Backward.Binary
366  for +a: Nat
367  for +b: Nat
368  for outside: {Nat.is_lt(b, List.length(&2, Backward.Entry, entries)) == False{} : Bool}
369  {Backward.binary(Backward.Tape{entries}, kind, a, b) == (Backward.Tape{entries}, Fail{Backward.UnknownNode{}}) :
370    Backward.Tape & Result<&2, &2, Backward.Error, Nat>}