@@ -1,6 +1,7 @@
1module Data.BoundedList
1module Data.BoundedList
3import Data.Fin
3import Data.Fin
5%access public export
6%access public export
6%default total
7%default total
@@ -50,6 +51,20 @@ fromList : (xs : List a) -> BoundedList (length xs) a
50fromList [] = []
51fromList [] = []
51fromList (x :: xs) = x :: fromList xs
52fromList (x :: xs) = x :: fromList xs
54+--------------------------------------------------------------------------------
55+-- Conversions to and from vector
56+--------------------------------------------------------------------------------
58+||| Convert bounded list to vector.
59+toVect : (xs : BoundedList n a) -> Vect (finToNat (length xs)) a
61+toVect (x :: xs) = x :: toVect xs
63+||| Convert vector to bounded list.
64+fromVect : (xs : Vect n a) -> BoundedList n a
66+fromVect (x :: xs) = x :: fromVect xs
53--------------------------------------------------------------------------------
68--------------------------------------------------------------------------------
54-- Building (bigger) bounded lists
69-- Building (bigger) bounded lists
55--------------------------------------------------------------------------------
70--------------------------------------------------------------------------------