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 #