law split_length

lawful-fields@0.1.1.0 · LAWS.bend:78

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

78# The number of pieces split gives is one more than the number of separators.
79law split_length:
80  for xs: List<&2, U32>
81  for sep: U32
82  {List.length(&2, List<&2, U32>, F.split(xs, sep)) == Nat.add(F.count(xs, sep), 1n) : Nat}