def list

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

import Base

90# [], chunk deletions (halves down to single elements), then single-element simplifications.
91def list(~A: Data, ~shrink: A -> List<&1, A>, xs: List<&2, A>) -> List<&1, List<&2, A>>:
92  +ys = xs
93  +n = List.length(&2, A, ys)
94  List.append(&1, List<&2, A>, list.dels(A, n, Nat.is_eq(n, 0n), n, n, ys),
95    list.ones(~A, ~shrink, ys))