Safe Haskell | Safe |
---|---|

Language | Haskell2010 |

This module provides type-level functions that need proofs to work properly.

# Documentation

hgcastWith :: forall (a :: k) (b :: k') (r :: Type). (a :~~: b) -> (a ~~ b => r) -> r Source #

Same as `gcastWith`

but for heterogeneous propositional
equality

# Concatenation of type-level lists

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 ProofNil xs where Source #

Proof that appending an empty list to any list has no effect on the latter.

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.

## Instances

Proof ([] :: [k]) (y :: k) (zs :: [k]) Source # | |

Proof ([] :: [k]) (y :: k) ([] :: [k]) Source # | |

ProofNil (xs ++ (y ': ([] :: [k]))) => Proof (x ': xs :: [k]) (y :: k) ([] :: [k]) Source # | |

Proof xs y (z ': zs) => Proof (x ': xs :: [a]) (y :: a) (z ': zs :: [a]) Source # | Induction on the tail of the list |