@@ -9,6 +9,7 @@ module TypeFun.Data.List
99 , Drop
1010 , Take
1111 , Delete
12+ , (:++:)
1213 -- * Elements lookup
1314 , IndexOf
1415 , IndexOfMay
@@ -91,6 +92,10 @@ type family Delete (a :: k) (s :: [k]) :: [k] where
9192 Delete a (a ': as) = Delete a as
9293 Delete a (b ': as) = b ': (Delete a as)
9394
95+type family (:++:) (a :: [k]) (b :: [k]) :: [k] where
96+ '[] :++: b = b
97+ (a ': as) :++: b = a ': (as :++: b)
98+
9499type IndexOf a s = FromJust (IndexOfMay a s)
95100
96101type IndexOfMay a s = IndexOfMay' Z a s