law byte_ext

lawful-words@0.1.0.0 · LAWS.bend:380

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

380# Two words with the same four bytes are the same word.
381law byte_ext:
382  for a: U32
383  for b: U32
384  for h0: {D.byte(a, 0n) == D.byte(b, 0n) : U32}
385  for h1: {D.byte(a, 1n) == D.byte(b, 1n) : U32}
386  for h2: {D.byte(a, 2n) == D.byte(b, 2n) : U32}
387  for h3: {D.byte(a, 3n) == D.byte(b, 3n) : U32}
388  {a == b : U32}