law get_after_set

bend-ml-tensor-array@0.1.19.0 · main.bend:2106

import Base

2106# LAW: what Array.set writes at i, Array.get reads at i (any i: both wrap it the same way)
2107law get_after_set:
2108  for -T: Data
2109  for a: Array<T>
2110  for +i: U32
2111  for +v: T
2112  {Pair.snd(Array<T>, T, Array.get(T, Array.set(T, a, i, v), i)) == v : T}