Safe Haskell	None
Language	GHC2021

Data.Type.Witness.Specific.Concat

Documentation

type family Concat (a :: [k]) (b :: [k]) :: [k] where ... Source #

Equations

Concat ('[] :: [k]) (bb :: [k]) = bb
Concat (a ': aa :: [k]) (bb :: [k]) = a ': Concat aa bb

concatEmptyRefl :: forall {k} (w :: k -> Type) (a :: [k]). ListType w a -> Concat a ('[] :: [k]) :~: a Source #

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)) Source #

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 Source #

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