law pl_r_le

lawful-bytes@0.1.1.0 · proof_list.bend:112

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

112# The run is no longer than the prefix.
113law pl_r_le:
114  for +zs: List<&2, U32>
115  for +n: Nat
116  for +c: U32
117  {Nat.is_le(D.run_len(List.take(&2, U32, zs, n), c), n) == True{} : Bool}