law sp2

lawful-fields@0.1.1.0 · proof_cut.bend:304

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

304# Without one, split gives ys itself.
305law sp2:
306  for +ys: List<&2, U32>
307  for +sep: U32
308  for +h: {Nat.is_le(List.length(&2, U32, ys), D.run_len(ys, sep)) == True{} : Bool}
309  {F.split(ys, sep) == [ys] : List<&2, List<&2, U32>>}