def to_nat_word

bend-collections-laws-math@1.0.0.0 · proofs/lib/u32.bend:18

import bend-collections-laws-math@1.0.0.0/proofs/lib/u32.bend as U32

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend as S
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/numeric.bend as RN

18def to_nat_word(+w: Word(32n)) -> {U32.to_nat(U32{w}) == S.unsigned(32n, w) : Nat}:
19  RN.primitive_word_interpretation(32n, w)

Uses (6)

Used by (15)