def uq.u32_shr

bend-osdev-algo@0.1.0.0 · proof_u32.bend:558

import bend-osdev-algo@0.1.0.0/proof_u32.bend as ProofU32

import Base

558def uq.u32_shr(a: U32) -> {U32.to_nat(U32.shr(a)) == uq.half(U32.to_nat(a)) : Nat}:
559  match a:
560    case U32{w}:
561      uq.shr_w(32n, w)

Uses (6)

Used by (1)

bend-osdev-algo@0.1.0.0/PROOF:ba.adv