~/jendhub

def wu.lt

bend-osdev-word64@0.1.1.0 · PROOF_bits.bend:20

import bend-osdev-word64@0.1.1.0/PROOF_bits.bend as PROOFBits
import Base
import bend-osdev-u32@0.1.0.0/u32.bend as U
import bend-osdev-u32@0.1.0.0/LAWS.bend as UL

20def wu.lt(+x: U32) -> {Nat.is_lt(U32.to_nat(x), U.U32Nat.dbl(32n, 1n)) == True{} : Bool}:
21  match x:
22    case U32{+w}:
23      %wu.ve(w) : {Nat.is_lt(_, U.U32Nat.dbl(32n, 1n)) == True{} : Bool}
24      UL.word_value_lt(32n, w)

Uses (7)

Used by (1)