~/jendhub

def below_zero

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

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

477def below_zero(+number: Nat) -> Holds<{Nat.is_lt(number, 0n) == False{} : Bool}>:
478  match number:
479    case 0n:
480      Holds{{==}}
481    case 1n+rest:
482      Holds{{==}}

Uses (4)

Used by (1)