law of_list_get

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

import Base
import bend-osdev-array@0.1.0.1/array.bend as A

180law of_list_get:
181  for -T: Data
182  for +d: Nat
183  for +xs: List<&2, T>
184  for +f: T
185  for +hl: {List.length(&2, T, xs) == A.Arrays.slots(d) : Nat}
186  for +hd: {Nat.is_lt(d, 32n) == True{} : Bool}
187  for +i: U32
188  {Array.get(T, A.Arrays.of_list(T, d, xs, f), i) == (A.Arrays.of_list(T, d, xs, f), A.Arrays.nth(T, xs, A.Arrays.index(d, i), f)) : Array<T> & T}