@@ -64,7 +64,7 @@ fromList [] = []
6464fromList (x::xs) = x :: fromList xs
6565
6666--------------------------------------------------------------------------------
67−-- Building bigger vectors
67+-- Building (bigger) vectors
6868--------------------------------------------------------------------------------
6969
7070total
@@ -72,6 +72,10 @@ total
7272(++) [] ys = ys
7373(++) (x::xs) ys = x :: xs ++ ys
7474
75+replicate : (n : Nat) -> a -> Vect a n
76+replicate O x = []
77+replicate (S k) x = x :: replicate k x
78+
7579--------------------------------------------------------------------------------
7680-- Maps
7781--------------------------------------------------------------------------------