law record_unknown_left

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

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

352# Recording with an operand id the tape does not hold is refused with
353# UnknownNode, and the tape comes back unchanged.
354law record_unknown_left:
355  for +entries: List<&2, Backward.Entry>
356  for kind: Backward.Binary
357  for +a: Nat
358  for +b: Nat
359  for outside: {Nat.is_lt(a, List.length(&2, Backward.Entry, entries)) == False{} : Bool}
360  {Backward.binary(Backward.Tape{entries}, kind, a, b) == (Backward.Tape{entries}, Fail{Backward.UnknownNode{}}) :
361    Backward.Tape & Result<&2, &2, Backward.Error, Nat>}