law get_set_same

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

import Base

34law get_set_same:
35  for -T: Data
36  for a: Array<T>
37  for i: U32
38  for v: T
39  {Pair.snd(Array<T>, T, Array.get(T, Array.set(T, a, i, v), i)) == v : T}