~/jendhub

def lt_succ_self

bendtorch-core@0.1.0.0 · src/autograd/gradient_PROOF.bend:53

import bendtorch-core@0.1.0.0/src/autograd/gradient_PROOF.bend as GradientPROOF
import Base

53def lt_succ_self(+number: Nat) -> {Nat.is_lt(number, 1n+number) == True{} : Bool}:
54  match number:
55    case 0n:
56      {==}
57    case 1n+rest:
58      lt_succ_self(rest)

Uses (3)

Used by (1)