law native_half_power

stelliferous@0.0.2.0 · proofs/word_power_of_two.bend:298

import Base

298law native_half_power:
299  for +depth: Nat
300  for fits: {Nat.is_lt(depth,31n) == True{} : Bool}
301  {U32.shr(U32.shln(1,1n+depth)) == U32.shln(1,depth) : U32}