@@ -1,6 +1,7 @@
11module Data.BoundedList
22
33import Data.Fin
4+import Data.Vect
45
56%access public export
67%default total
@@ -50,6 +51,20 @@ fromList : (xs : List a) -> BoundedList (length xs) a
5051fromList [] = []
5152fromList (x :: xs) = x :: fromList xs
5253
54+--------------------------------------------------------------------------------
55+-- Conversions to and from vector
56+--------------------------------------------------------------------------------
57+
58+||| Convert bounded list to vector.
59+toVect : (xs : BoundedList n a) -> Vect (finToNat (length xs)) a
60+toVect [] = []
61+toVect (x :: xs) = x :: toVect xs
62+
63+||| Convert vector to bounded list.
64+fromVect : (xs : Vect n a) -> BoundedList n a
65+fromVect [] = []
66+fromVect (x :: xs) = x :: fromVect xs
67+
5368--------------------------------------------------------------------------------
5469-- Building (bigger) bounded lists
5570--------------------------------------------------------------------------------