git.iko.soy/Idris-dev
on master help sign in
added replicate
ab12e51Mekeor Melire
lib/prelude/vect.idr+5−1
compare with master
unifiedsplit
@@ -64,7 +64,7 @@ fromList [] = []
64fromList (x::xs) = x :: fromList xs
64fromList (x::xs) = x :: fromList xs
65
65
66--------------------------------------------------------------------------------
66--------------------------------------------------------------------------------
67−-- Building bigger vectors
67+-- Building (bigger) vectors
68--------------------------------------------------------------------------------
68--------------------------------------------------------------------------------
69
69
70total
70total
@@ -72,6 +72,10 @@ total
72(++) [] ys = ys
72(++) [] ys = ys
73(++) (x::xs) ys = x :: xs ++ ys
73(++) (x::xs) ys = x :: xs ++ ys
74
74
75+replicate : (n : Nat) -> a -> Vect a n
76+replicate O x = []
77+replicate (S k) x = x :: replicate k x
78+
75--------------------------------------------------------------------------------
79--------------------------------------------------------------------------------
76-- Maps
80-- Maps
77--------------------------------------------------------------------------------
81--------------------------------------------------------------------------------