Data.Tuple.Morph.Append

Appending type lists and HLists.

Documentation

type family a ++ b :: [k] infixr 5

Appends two type lists.

Equations

[] ++ b = b

(a : as) ++ b = a : (as ++ b)

appendAssoc :: Proxy a -> Proxy b -> Proxy c -> ((a ++ b) ++ c) :~: (a ++ (b ++ c))

Proof (by unsafeCoerce) that appending is associative.

appendRightId :: Proxy a -> (a ++ []) :~: a

Proof (by unsafeCoerce) that '[] is a right identity of (++).

(++@) :: HList a -> HList b -> HList (a ++ b) infixr 5

Appends two HLists.