law get_set_same

lawful-arrays@0.1.0.0 · LAWS.bend:99

import Base

99# Reading what was just written gives it back.
100# (This holds for every tree: set and get take the same path.)
101law get_set_same:
102  for -T: Data
103  for a: Array<T>
104  for i: U32
105  for v: T
106  {Pair.snd(Array<T>, T, Array.get(T, Array.set(T, a, i, v), i)) == v : T}