~/jendhub

def lt_self_succ

bendtorch-core@0.1.0.0 · src/autograd/reduce_fiber_proof.bend:352

import bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend as ReduceFiberProof
import Base

352def lt_self_succ(+k: Nat) -> {Nat.is_lt(k, 1n+k) == True{} : Bool}:
353  match k:
354    case 0n:
355      {==}
356    case 1n+p:
357      lt_self_succ(p)

Uses (3)

Used by (1)