law byte_ext

lawful-words@0.1.0.0 · proof_bytes.bend:1345

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

1345law byte_ext:
1346  for +a: U32
1347  for +b: U32
1348  for +h0: {D.byte(a, 0n) == D.byte(b, 0n) : U32}
1349  for +h1: {D.byte(a, 1n) == D.byte(b, 1n) : U32}
1350  for +h2: {D.byte(a, 2n) == D.byte(b, 2n) : U32}
1351  for +h3: {D.byte(a, 3n) == D.byte(b, 3n) : U32}
1352  {a == b : U32}