def wu.lt

bend-osdev-word64@0.1.1.0 · PROOF_text.bend:22

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

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