law at_pair

lawful-bytes@0.1.1.0 · LAWS.bend:75

import Base
import lawful-bytes@0.1.1.0/defs.bend as D
import lawful-bytes@0.1.1.0/bytes.bend as B

75# The result as a literal pair: the same Bytes and the value (for rewriting).
76law at_pair:
77  for b: D.Bytes
78  for i: U32
79  {B.at(b, i) == (b, Pair.snd(D.Bytes, U32, B.at(b, i))) : D.Bytes & U32}