def full

lawful-arrays@0.1.0.0 · defs.bend:9

import Base

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