def Chapter8.splits {α : Type u_1} : List α → List (List α × List α)

Equations

• Chapter8.splits [] = []
• Chapter8.splits (x_1 :: xs) = ([], x_1 :: xs) :: List.map (fun (x : List α × List α) => match x with | (ys, zs) => (x_1 :: ys, zs)) (Chapter8.splits xs)

def Chapter8.splitsn {α : Type u_1} : List α → List (List α × List α)

Equations

• Chapter8.splitsn [] = []
• Chapter8.splitsn [head] = []
• Chapter8.splitsn (x_1 :: xs) = ([x_1], xs) :: List.map (fun (x : List α × List α) => match x with | (ys, zs) => (x_1 :: ys, zs)) (Chapter8.splitsn xs)