Data.Type.Index

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

Documentation

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

Constructors

IZ :: Index (a :< as) a

IS :: !(Index as a) -> Index (b :< as) a

Instances

TestEquality k (Index k as)

Show1 k (Index k as)

Ord1 k (Index k as)

Eq1 k (Index k as)

Known k (Index k as) a => Known k (Index k ((:<) k b as)) a

Known k (Index k ((:<) k a as)) a

Read2 [k] k (Index k)

IxTraversable1 [k] k (Index k) (Sum k)

IxTraversable1 [k] k (Index k) (Prod k)

IxFoldable1 [k] k (Index k) (Sum k)

IxFoldable1 [k] k (Index k) (Prod k)

IxFunctor1 [k] k (Index k) (Sum k)

IxFunctor1 [k] k (Index k) (Prod k)

Eq (Index k as a)

Ord (Index k as a)

Show (Index k as a)

type KnownC k (Index k ((:<) k b as)) a = ØC

type KnownC k (Index k ((:<) k a as)) a = ØC

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

ixNil :: Index Ø a -> Void

onIxPred :: (Index as a -> Index bs a) -> Index (b :< as) a -> Index (b :< bs) a

type (∈) a as = Elem as a infix 6

class Elem as a where

Methods

elemIndex :: Index as a

Instances

Elem k as a => Elem k ((:<) k b as) a

Elem k ((:<) k a as) a