law wl

lawful-fields@0.1.1.0 · proof_cut.bend:609

import Base
import lawful-fields@0.1.1.0/defs.bend as F

609# The ends of split(ys) from s lie in s .. s + length(ys).
610law wl:
611  for +ys: List<&2, U32>
612  for +s: Nat
613  for +sep: U32
614  {WN(F.ends(F.split(ys, sep), s), s, Nat.add(s, List.length(&2, U32, ys))) == True{} : Bool}