@@ -0,0 +1,42 @@
1+module Data.BoundedList
2+
3+%default total
4+
5+data BoundedList : Type -> Nat -> Type where
6+ Nil : BoundedList a n
7+ (::) : a -> BoundedList a n -> BoundedList a (S n)
8+
9+length : BoundedList a n -> Fin (S n)
10+length [] = fO
11+length (x :: xs) = fS (length xs)
12+
13+index : Fin (S n) -> BoundedList a n -> Maybe a
14+index _ [] = Nothing
15+index fO (x :: _) = Just x
16+index (fS f) (_ :: xs) = index f xs
17+
18+weaken : BoundedList a n -> BoundedList a (n + m)
19+weaken [] = []
20+weaken (x :: xs) = x :: weaken xs
21+
22+take : (n : Nat) -> List a -> BoundedList a n
23+take _ [] = []
24+take O _ = []
25+take (S n') (x :: xs) = x :: take n' xs
26+
27+toList : BoundedList a n -> List a
28+toList [] = []
29+toList (x :: xs) = x :: toList xs
30+
31+fromList : (xs : List a) -> BoundedList a (length xs)
32+fromList [] = []
33+fromList (x :: xs) = x :: fromList xs
34+
35+map : (a -> b) -> BoundedList a n -> BoundedList b n
36+map f [] = []
37+map f (x :: xs) = f x :: map f xs
38+
39+zeroBoundIsEmpty : (xs : BoundedList a 0) -> xs = the (BoundedList a 0) []
40+zeroBoundIsEmpty [] = refl
41+zeroBoundIsEmpty (_ :: _) impossible
42+