law to_nat_shr
import lawful-words@0.1.0.0/LAWS.bend as LAWSimport Base
191law to_nat_shr:
192 for a: U32
193 {U32.to_nat(U32.shr(a)) == Nat.div(U32.to_nat(a), 2n) : Nat}
Uses (6)
Used by (0)
No other definition uses this definition.
import lawful-words@0.1.0.0/LAWS.bend as LAWSimport Base
191law to_nat_shr:
192 for a: U32
193 {U32.to_nat(U32.shr(a)) == Nat.div(U32.to_nat(a), 2n) : Nat}
No other definition uses this definition.