law set_keeps_size

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

import Base

41law set_keeps_size:
42  for -T: Data
43  for a: Array<T>
44  for i: U32
45  for v: T
46  {Pair.snd(Array<T>, U32, Array.size(T, Array.set(T, a, i, v))) == Pair.snd(Array<T>, U32, Array.size(T, a)) : U32}