Commit 2020-05-04 10:57 14aa1f7b
View on Github →feat(combinatorics/composition): refactor compositions, split a list wrt a composition (#2554)
Refactor composition, replacing in its definition a list of positive integers with a list of integers which are positive. This avoids going back and forth all the time between nat and pnat.
Also introduce the ability to split a list of length n with respect to a composition c of n, giving rise to a list of c.length sublists whose join is the original list.