~/jendhub

def un.u32_shl_low

bend-osdev-u32@0.1.0.0 · PROOF.bend:2235

import bend-osdev-u32@0.1.0.0/PROOF.bend as PROOF
import Base
import bend-osdev-u32@0.1.0.0/u32.bend as U

2235def un.u32_shl_low(+x: U32) -> {U32.to_nat(U32.shl(x)) == U.U32Nat.low(32n, Nat.double(U32.to_nat(x))) : Nat}:
2236  match x:
2237    case U32{+v}:
2238      un.shl_low(32n, v)

Uses (7)

Used by (1)