Defs.full: def of lawful-arrays@0.1.0.0
Import: import lawful-arrays@0.1.0.0/defs.bend as Defs
Lines 9-20 of lawful-arrays@0.1.0.0/defs.bend: https://jend.leeeet.dev/read.txt?path=lawful-arrays@0.1.0.0/defs.bend&start_line=9&end_line=20

import Base

# a is a perfect tree of depth d: 2^d leaves, every one at depth d. Arrays
# made by Array.new are; Array.set and Array.get keep it so.
def full(-T: Type, a: Array<T>, +d: Nat) -> Bool:
  match a d:
    case ALeaf{x} 0n:
      True{}
    case ALeaf{x} 1n+p:
      False{}
    case ANode{xs, ys} 0n:
      False{}
    case ANode{xs, ys} 1n+p:
      full(T, xs, p) && full(T, ys, p)

Uses (4):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.and
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat