~/jendhub

def wsd.mul16

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

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

116def wsd.mul16(+x: U32) -> {U32.to_nat(U32.mul(x, 65536)) == U.U32Nat.low(32n, U.U32Nat.dbl(16n, U32.to_nat(x))) : Nat}:
117  match x:
118    case U32{+w}:
119      wsd.mulpw(32n, 16n, w, {==})

Uses (7)

Used by (1)