law set_length

bend-osdev-array@0.1.0.1 · LAWS.bend:218

import Base

218law set_length:
219  for -T: Data
220  for xs: List<&2, T>
221  for k: Nat
222  for v: T
223  {List.length(&2, T, List.set(&2, T, xs, k, v)) == List.length(&2, T, xs) : Nat}