law wrap_small

lawful-words@0.1.0.0 · LAWS.bend:36

import Base

36# A number below 2^32 is unchanged by wrapping.
37law wrap_small:
38  for n: Nat
39  for h: {Nat.is_lt(n, Nat.pow(2n, 32n)) == True{} : Bool}
40  {Nat.mod(n, Nat.pow(2n, 32n)) == n : Nat}