def older_ne

bendtorch-core@0.1.0.0 · src/autograd/tensor_backward_PROOF.bend:39

import Base

39# A node with older nodes below it and extra + 1 newer ones above it never has
40# the id of the target.
41def older_ne(+older: Nat, -extra: Nat) -> {False{} == Nat.is_eq(Nat.add(older, 1n+extra), older) : Bool}:
42  match older:
43    case 0n:
44      {==}
45    case 1n+rest:
46      older_ne(rest, extra)