def u32_val
import bend-collections-laws-math@1.0.0.0/spec/math/generic.bend as Genericimport Base
276# ---- instance models ----
277# U32: the value and the U32 of a value below 2^32 (width 32)
278def u32_val(x: U32) -> Nat:
279 U32.to_nat(x)
Uses (3)
Used by (203)
- bend-collections-laws-math@1.0.0.0/proofs/math/typed/u32int:v
- bend-collections-laws-math@1.0.0.0/proofs/math/typed/fix32:mul_low
- bend-collections-laws-math@1.0.0.0/proofs/math/typed/fix32:pw
- bend-collections-laws-math@1.0.0.0/proofs/math/typed/u32laws:ops_sub
- bend-collections-laws-math@1.0.0.0/proofs/math/typed/u32laws:tests_odd
- …