law of_list_leaves

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

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

165law of_list_leaves:
166  for -T: Data
167  for +d: Nat
168  for +xs: List<&2, T>
169  for +f: T
170  for +hl: {List.length(&2, T, xs) == A.Arrays.slots(d) : Nat}
171  {A.Arrays.leaves(T, A.Arrays.of_list(T, d, xs, f)) == xs : List<&2, T>}