def wv.lt64

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

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

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