law fast_find_pair

lawful-bytes@0.1.1.0 · LAWS.bend:443

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

443# The fast searches hand back the same Bytes, for any arguments (as find_pair
444# and find2_pair say of the reference).
445law fast_find_pair:
446  for b: D.Bytes
447  for from: U32
448  for to: U32
449  for c: U32
450  {FA.find(b, from, to, c) == (b, Pair.snd(D.Bytes, U32, FA.find(b, from, to, c))) : D.Bytes & U32}