law sp1

lawful-fields@0.1.1.0 · proof_cut.bend:267

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

267# With a separator in ys, the first piece ends at it.
268law sp1:
269  for +ys: List<&2, U32>
270  for +sep: U32
271  for +h: {Nat.is_lt(D.run_len(ys, sep), List.length(&2, U32, ys)) == True{} : Bool}
272  {F.split(ys, sep) == List.take(&2, U32, ys, D.run_len(ys, sep)) <> F.split(List.drop(&2, U32, ys, Nat.add(D.run_len(ys, sep), 1n)), sep) : List<&2, List<&2, U32>>}