def Lake.List.squeeze {α : Type u_1} [BEq α] : List α → List α

Remove adjacent duplicates.

Equations

• Lake.List.squeeze [] = []
• Lake.List.squeeze (x' :: xs') = match Lake.List.squeeze xs' with | [] => [x'] | x'_1 :: xs' => if (x' == x'_1) = true then x'_1 :: xs' else x' :: x'_1 :: xs'