def vb
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/u32laws.bend as U32lawsimport Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
42# every U32 value fits 32 bits
43def vb(+x: U32) -> {C.fits(32n, v(x)) == True{} : Bool}:
44 vb_k(32n, {==}, x)
Uses (5)
Used by (53)
- bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64add:vb
- bend-collections-laws-math@1.0.0.0/proofs/math/typed/u64laws:vb
- bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64cmp:hF
- bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64light:vb64
- bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64bits:half0
- …