~/jendhub

def older_ne

bendtorch-core@0.1.0.0 · src/autograd/tensor_chain_PROOF.bend:490

import bendtorch-core@0.1.0.0/src/autograd/tensor_chain_PROOF.bend as TensorChainPROOF
import Base

490# A node with older nodes below it and extra + 1 newer ones above it never has
491# the id of the target.
492def older_ne(+older: Nat, -extra: Nat) -> {False{} == Nat.is_eq(Nat.add(older, 1n+extra), older) : Bool}:
493  match older:
494    case 0n:
495      {==}
496    case 1n+rest:
497      older_ne(rest, extra)

Uses (4)

Used by (1)