def vw

bend-collections-laws-crypto@1.0.0.0 · proofs/lib/u32div.bend:61

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32.bend as U
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend as WD

61def vw(+w: Word(32n)) -> {v(U32{w}) == WD.uw(32n, w) : Nat}:
62  U.to_nat_word(w)