law pieces_length

lawful-fields@0.1.1.0 · LAWS.bend:163

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

163law pieces_length:
164  for es: List<&2, U32>
165  for xs: List<&2, U32>
166  for from: Nat
167  {List.length(&2, List<&2, U32>, F.pieces(es, xs, from)) == List.length(&2, U32, es) : Nat}