law first_hit

lawful-bytes@0.1.1.0 · LAWS.bend:344

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

344# Below to, the answer holds c.
345law first_hit:
346  for xs: List<&2, U32>
347  for from: Nat
348  for to: Nat
349  for c: U32
350  for hft: {Nat.is_le(from, to) == True{} : Bool}
351  for ht: {Nat.is_le(to, List.length(&2, U32, xs)) == True{} : Bool}
352  for hlt: {Nat.is_lt(D.first(xs, from, to, c), to) == True{} : Bool}
353  {D.has(xs, D.first(xs, from, to, c), c) == True{} : Bool}