def bounded

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

import Base

86# Operand bounds, stated without the engine's validator: a node may name only
87# nodes older than itself, so each operand id must be below the number of
88# older nodes. An operand that is the node itself, a newer node or a missing
89# node fails this bound.
90def bounded(ids: List<&2, Nat>, +bound: Nat) -> Bool:
91  match ids:
92    case Nil{}:
93      True{}
94    case Con{+id, rest}:
95      Bool.and(Nat.is_lt(id, bound), bounded(rest, bound))