From 8cd56f32ab90bccab06957fbb3329490dd1929d3 Mon Sep 17 00:00:00 2001 From: Nathan McCarty Date: Sun, 19 Jan 2025 17:51:56 -0500 Subject: [PATCH] Add rotations to Util --- src/Util.md | 23 +++++++++++++++++++++++ 1 file changed, 23 insertions(+) diff --git a/src/Util.md b/src/Util.md index 1d46e9e..836a4cd 100644 --- a/src/Util.md +++ b/src/Util.md @@ -51,6 +51,29 @@ contains x (y :: xs) = else contains x xs ``` +### rotations + +Provides all the 'rotations' of a list. + +Example: + +``` +rotations [1, 2, 3] == [[1, 2, 3], [3, 1, 2], [2, 3, 1]] +``` + +```idris +export +rotations : List a -> List (List a) +rotations xs = rotations' (length xs) xs [] + where + rotations' : Nat -> List a -> (acc : List (List a)) -> List (List a) + rotations' 0 xs acc = acc + rotations' (S k) [] acc = acc + rotations' (S k) (x :: xs) acc = + let next = xs ++ [x] + in rotations' k next (next :: acc) +``` + ## Vectors Define some operations for pairs of numbers, treating them roughly like vectors