Safe Haskell | Safe |
---|---|
Language | Haskell2010 |
This module provides type-level functions that need proofs to work properly.
Documentation
type family (xs :: [k]) ++ (ts :: [k]) = (res :: [k]) where ... Source #
Append two type-level lists
> :kind! '[Int, Bool] ++ '[Char, Maybe Int] '[Int, Bool, Char, Maybe Int]
class Proof xs y zs where Source #
Proof that appending two lists is the same as appending the first element of the second list to the first one, and then appending the rest.