law first_range

lawful-bytes@0.1.1.0 · LAWS.bend:335

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

335law first_range:
336  for xs: List<&2, U32>
337  for from: Nat
338  for to: Nat
339  for c: U32
340  for hft: {Nat.is_le(from, to) == True{} : Bool}
341  for ht: {Nat.is_le(to, List.length(&2, U32, xs)) == True{} : Bool}
342  {(Nat.is_le(from, D.first(xs, from, to, c)) && Nat.is_le(D.first(xs, from, to, c), to)) == True{} : Bool}