law bit_ext

lawful-words@0.1.0.0 · LAWS.bend:312

import Base
import lawful-words@0.1.0.0/defs.bend as D

312# Two words with the same bits are the same word.
313law bit_ext:
314  for a: U32
315  for b: U32
316  for h: @k: Nat -> {D.bit(a, k) == D.bit(b, k) : Bool}
317  {a == b : U32}