Copyright	Copyright (C) 2015 Kyle Carter
License	BSD3
Maintainer	Kyle Carter <kylcarte@indiana.edu>
Stability	experimental
Portability	RankNTypes
Safe Haskell	None
Language	Haskell2010

Data.Type.Index

Description

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

Documentation

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

Constructors

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

Instances

Known k (Index k as) a => Known k (Index k ((:<) k b as)) a Source
Known k (Index k ((:<) k a as)) a Source
HIxTraversable [k] k (Index k) (Sum k) Source
HIxFoldable [k] k (Index k) (Sum k) Source
HIxFoldable [k] k (Index k) (Prod k) Source
HIxFunctor [k] k (Index k) (Sum k) Source
HIxFunctor [k] k (Index k) (Prod k) Source
Eq (Index k as a) Source
Ord (Index k as a) Source
Show (Index k as a) Source
type KnownC k (Index k ((:<) k b as)) a = ØC
type KnownC k (Index k ((:<) k a as)) a = ØC

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

class Elem as a where Source

Methods

Instances

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