~/jendhub

def wv.lt64

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

import bend-osdev-word64@0.1.1.0/PROOF_text.bend as PROOFText
import Base
import bend-osdev-u32@0.1.0.0/u32.bend as U
import bend-osdev-word64@0.1.1.0/word64.bend as W

36def wv.lt64(+x: W.W64) -> {Nat.is_lt(W.W64.to_nat(x), U.U32Nat.dbl(64n, 1n)) == True{} : Bool}:
37  match x:
38    case W.W64{U32{+h}, U32{+l}}:
39      %wv.ve(h, l) : {Nat.is_lt(_, U.U32Nat.dbl(64n, 1n)) == True{} : Bool}
40      wv.g(32n, 64n, h, l, {==})

Uses (8)

Used by (1)