Copyright | Copyright (C) 2015 Kyle Carter |
---|---|

License | BSD3 |

Maintainer | Kyle Carter <kylcarte@indiana.edu> |

Stability | experimental |

Portability | RankNTypes |

Safe Haskell | None |

Language | Haskell2010 |

A `singleton`

-esque type for representing indices in a type-level list.

# Documentation

data Index :: [k] -> k -> * where Source #

Read2 l [l] (Index l) Source # | |

IxTraversable1 k [k] (Index k) (Sum k) Source # | |

IxTraversable1 k [k] (Index k) (Prod k) Source # | |

IxFoldable1 k [k] (Index k) (Sum k) Source # | |

IxFoldable1 k [k] (Index k) (Prod k) Source # | |

IxFunctor1 k [k] (Index k) (Sum k) Source # | |

IxFunctor1 k [k] (Index k) (Prod k) Source # | |

TestEquality k (Index k as) Source # | |

Show1 k (Index k as) Source # | |

Ord1 k (Index k as) Source # | |

Eq1 k (Index k as) Source # | |

(∈) k a as => Known k (Index k as) a Source # | |

Witness ØC (Elem k as a) (Index k as a) Source # | |

Eq (Index k as a) Source # | |

Ord (Index k as a) Source # | |

Show (Index k as a) Source # | |

type KnownC k (Index k as) a Source # | |

type WitnessC ØC (Elem k as a) (Index k as a) Source # | |

elimIndex :: (forall xs. p (a :< xs) a) -> (forall x xs. Index xs a -> p xs a -> p (x :< xs) a) -> Index as a -> p as a Source #