law of_list_size

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

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

173law of_list_size:
174  for -T: Data
175  for +d: Nat
176  for +xs: List<&2, T>
177  for +f: T
178  {Array.size(T, A.Arrays.of_list(T, d, xs, f)) == (A.Arrays.of_list(T, d, xs, f), U32.shln(1, d)) : Array<T> & U32}