~/jendhub

def vw

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

import bend-collections-laws-math@1.0.0.0/proofs/lib/u32div.bend as U32div
import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/u32.bend as U
import bend-collections-laws-math@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)

Uses (6)

Used by (18)