law to_nat_shrn
import lawful-words@0.1.0.0/LAWS.bend as LAWSimport Base
199law to_nat_shrn:
200 for a: U32
201 for k: Nat
202 {U32.to_nat(U32.shrn(a, k)) == Nat.div(U32.to_nat(a), Nat.pow(2n, k)) : Nat}
Uses (7)
Used by (0)
No other definition uses this definition.