law cmp_bits

bend-lawful-stdlib@0.1.0.0 · src/u32.bend:22

import Base
import bend-lawful-stdlib@0.1.0.0/src/nat.bend as Nat

22# comparing bit + 2*rest compares the rests first, then the bits, which is
23# what Word.cmp.fin does
24law cmp_bits:
25  for x: Bool
26  for y: Bool
27  for a: Nat
28  for b: Nat
29  {Word.cmp.fin(x, y, Nat.cmp(a, b)) == Nat.cmp(Nat.add(bit(x), Nat.double(a)), Nat.add(bit(y), Nat.double(b))) : Cmp}