law get_new

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

import Base

48law get_new:
49  for -T: Data
50  for d: Nat
51  for v: T
52  for i: U32
53  {Pair.snd(Array<T>, T, Array.get(T, Array.new(T, d, v), i)) == v : T}