law native_power_bound

stelliferous@0.0.2.0 · proofs/word_power_of_two.bend:308

import Base

308law native_power_bound:
309  for +depth: Nat
310  for bound: {Nat.is_le(depth,31n) == True{} : Bool}
311  {U32.is_le(U32.shln(1,depth),2147483648) == True{} : Bool}