~/jendhub

def wu.lt

bend-osdev-word64@0.1.1.0 · PROOF_div.bend:24

import bend-osdev-word64@0.1.1.0/PROOF_div.bend as PROOFDiv
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

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

Uses (7)

Used by (1)