From 0fc8fa7e18d0f39c665127206fcac29cc78fb5dc Mon Sep 17 00:00:00 2001
From: Nathan McCarty <thatonelutenist@stranger.systems>
Date: Sun, 16 Feb 2025 04:03:28 -0500
Subject: [PATCH] Add listToVect to util

---
 src/Util.md | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/src/Util.md b/src/Util.md
index 9264794..7d1342e 100644
--- a/src/Util.md
+++ b/src/Util.md
@@ -192,6 +192,14 @@ Lazily generate all the permutations of a Vect
   maxBy f (x :: xs) = Foldable.maxBy f x xs
 ```
 
+### Convert a list to a vect as a sigma type
+
+```idris
+  export
+  listToVect : List a -> (n : Nat ** Vect n a)
+  listToVect xs = (length xs ** fromList xs)
+```
+
 ## Fin
 
 ```idris hide