law cmp_to_nat

lawful-words@0.1.0.0 · LAWS.bend:46

import Base

46# Words compare as their numbers; every U32.is_* test follows from this one.
47law cmp_to_nat:
48  for a: U32
49  for b: U32
50  {U32.cmp(a, b) == Nat.cmp(U32.to_nat(a), U32.to_nat(b)) : Cmp}