def wv.lt64

bend-osdev-word64@0.1.1.0 · PROOF_mul.bend:34

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

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