Add rotations to Util

This commit is contained in:
Nathan McCarty 2025-01-19 17:51:56 -05:00
parent d343cc37a3
commit 8cd56f32ab

View file

@ -51,6 +51,29 @@ contains x (y :: xs) =
else contains x 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 ## Vectors
Define some operations for pairs of numbers, treating them roughly like vectors Define some operations for pairs of numbers, treating them roughly like vectors