Data.Type.Witness.Specific.Concat

Documentation

type family Concat a b where ...

Equations

Concat '[] bb = bb

Concat (a ': aa) bb = a ': Concat aa bb

concatEmptyRefl :: ListType w a -> Concat a '[] :~: a

concatIsDict :: forall k (w :: k -> Type) (aa :: [k]) (bb :: [k]). (Representative w, Is (ListType w) aa, Is (ListType w) bb) => Dict (Is (ListType w) (Concat aa bb))

withConcatIs :: forall k (w :: k -> Type) (aa :: [k]) (bb :: [k]) r. (Representative w, Is (ListType w) aa, Is (ListType w) bb) => (Is (ListType w) (Concat aa bb) => r) -> r

concatListType :: forall k (w :: k -> Type) (a :: [k]) (b :: [k]). ListType w a -> ListType w b -> ListType w (Concat a b)