law pl_r_hit

lawful-bytes@0.1.1.0 · proof_list.bend:149

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

149# Short of the end, the run stops at a c.
150law pl_r_hit:
151  for +zs: List<&2, U32>
152  for +n: Nat
153  for +c: U32
154  for +ht: {Nat.is_le(n, List.length(&2, U32, zs)) == True{} : Bool}
155  for +hlt: {Nat.is_lt(D.run_len(List.take(&2, U32, zs, n), c), n) == True{} : Bool}
156  {D.has(zs, D.run_len(List.take(&2, U32, zs, n), c), c) == True{} : Bool}