def ne_succ

bendtorch-core@0.1.0.0 · src/autograd/sgd_PROOF.bend:107

import Base

107# A list of n nodes never has id n + 1 + extra at its head.
108def ne_succ(+number: Nat, -extra: Nat) -> {False{} == Nat.is_eq(number, 1n+Nat.add(number, extra)) : Bool}:
109  match number:
110    case 0n:
111      {==}
112    case 1n+rest:
113      ne_succ(rest, extra)