law get_new

lawful-arrays@0.1.0.0 · LAWS.bend:184

import Base

184# A new array reads as its initial value everywhere (every depth, every index).
185law get_new:
186  for -T: Data
187  for d: Nat
188  for v: T
189  for i: U32
190  {Pair.snd(Array<T>, T, Array.get(T, Array.new(T, d, v), i)) == v : T}