~/jendhub

def below_self

bendtorch-core@0.1.0.0 · src/autograd/reduce_PROOF.bend:506

import bendtorch-core@0.1.0.0/src/autograd/reduce_PROOF.bend as ReducePROOF
import Base

506def below_self(+number: Nat) -> {Nat.is_lt(number, number) == False{} : Bool}:
507  match number:
508    case 0n:
509      {==}
510    case 1n+rest:
511      below_self(rest)

Uses (3)

Used by (1)