law digits_pair

lawful-fields@0.1.1.0 · LAWS.bend:102

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

102law digits_pair:
103  for b: D.Bytes
104  for from: U32
105  for to: U32
106  {C.digits(b, from, to) == (b, Pair.snd(D.Bytes, Bool, C.digits(b, from, to))) : D.Bytes & Bool}