Array.Arrays.of_list: def of bend-osdev-array@0.1.0.1
Import: import bend-osdev-array@0.1.0.1/array.bend as Array
Lines 60-69 of bend-osdev-array@0.1.0.1/array.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-array@0.1.0.1/array.bend&start_line=60&end_line=69

import Base

# The perfect array of depth d whose slots are xs in order (cut to 2^d
# slots, or padded with fill): an array built from a Data list, so that a
# proof can name it as often as it likes (a specification, like leaves)
def Arrays.of_list(-T: Data, +d: Nat, +xs: List<&2, T>, +fill: T) -> Array<T>:
  match d:
    case 0n:
      ALeaf{Arrays.nth(T, xs, 0n, fill)}
    case 1n+p:
      +s = Arrays.slots(p)
      ANode{Arrays.of_list(T, p, List.take(&2, T, xs, s), fill), Arrays.of_list(T, p, List.drop(&2, T, xs, s), fill)}

Uses (7):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.drop
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.take
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/array.bend&name=Arrays.nth
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/array.bend&name=Arrays.slots