def list.dels

bend-kit-property@0.4.0.0 · shrink.bend:55

import Base

55# Chunk deletions for k = n, n/2, ..., 1; k = n is the lone candidate [].
56def list.dels(-A: Data, f: Nat, stop: Bool, +k: Nat, +n: Nat, +xs: List<&2, A>) -> List<&1, List<&2, A>>:
57  match f stop:
58    case 0n _:
59      Nil{}
60    case 1n+p True{}:
61      Nil{}
62    case 1n+p False{}:
63      +h = Nat.div(k, 2n)
64      List.append(&1, List<&2, A>, list.chunks(A, n, Nat.is_gt(k, n), 0n, k, n, xs),
65        list.dels(A, p, Nat.is_eq(h, 0n), h, n, xs))