~/jendhub

def lt_self_succ

bendtorch-core@0.1.0.0 · src/autograd/reduce_replayed_proof.bend:144

import bendtorch-core@0.1.0.0/src/autograd/reduce_replayed_proof.bend as ReduceReplayedProof
import Base

144def lt_self_succ(+k: Nat) -> {Nat.is_lt(k, 1n+k) == True{} : Bool}:
145  match k:
146    case 0n:
147      {==}
148    case 1n+p:
149      lt_self_succ(p)

Uses (3)

Used by (1)