~/jendhub

def limit_not_below

bendtorch-core@0.1.0.0 · src/tensor/signed_PROOF.bend:128

import bendtorch-core@0.1.0.0/src/tensor/signed_PROOF.bend as SignedPROOF
import Base
import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith

128# limit is not below itself.
129def limit_not_below(+limit: U32) -> {U32.is_lt(limit, limit) == False{} : Bool}:
130  Equal.trans(Bool, U32.is_lt(limit, limit), Nat.is_lt(U32.to_nat(limit), U32.to_nat(limit)), False{},
131    Equal.sym(Bool, Nat.is_lt(U32.to_nat(limit), U32.to_nat(limit)), U32.is_lt(limit, limit), Arith.u32_lt(limit, limit)),
132    lt_self(U32.to_nat(limit)))

Uses (9)

Used by (1)