law get_set_other

lawful-arrays@0.1.0.0 · LAWS.bend:108

import Base
import lawful-arrays@0.1.0.0/defs.bend as D

108# Writing leaf i does not change leaf j (j a different leaf modulo the size).
109law get_set_other:
110  for -T: Data
111  for a: Array<T>
112  for d: Nat
113  for i: U32
114  for j: U32
115  for v: T
116  for hf: {D.full(T, a, d) == True{} : Bool}
117  for hd: {Nat.is_lt(d, 32n) == True{} : Bool}
118  for hij: {Nat.is_eq(D.slot(i, d), D.slot(j, d)) == False{} : Bool}
119  {Pair.snd(Array<T>, T, Array.get(T, Array.set(T, a, i, v), j)) == Pair.snd(Array<T>, T, Array.get(T, a, j)) : T}