law sgd_refusal_unknown

bendtorch-core@0.1.0.0 · src/autograd/sgd_LAWS.bend:151

import Base
import bendtorch-core@0.1.0.0/src/autograd/tensor_backward.bend as Backward
import bendtorch-core@0.1.0.0/src/autograd/sgd.bend as Sgd

151# An id the tape does not hold, the number of its nodes or more, is refused
152# with UnknownNode.
153law sgd_refusal_unknown:
154  for nodes: List<&2, Backward.Node>
155  for +extra: Nat
156  {Sgd.refusal_at(nodes, List.length(&2, Backward.Node, nodes), Nat.add(List.length(&2, Backward.Node, nodes), extra),
157      Backward.at_head(List.length(&2, Backward.Node, nodes), Nat.add(List.length(&2, Backward.Node, nodes), extra))) ==
158    Some{Sgd.UnknownNode{}} : Maybe<&2, Sgd.Error>}