Data.Type.Witness.Specific.List.Element

Documentation

data ListElementType kk t where

Constructors

FirstElementType :: ListElementType (t ': tt) t

RestElementType :: ListElementType aa t -> ListElementType (a ': aa) t

Instances

TestEquality (ListElementType tt :: k -> Type)

Defined in Data.Type.Witness.Specific.List.Element

Methods

testEquality :: forall (a :: k0) (b :: k0). ListElementType tt a -> ListElementType tt b -> Maybe (a :~: b)

Is (ListType (Proxy :: k -> Type)) tt => ListElementWitness (ListElementType tt :: k -> Type)

Defined in Data.Type.Witness.General.ListElement

Associated Types

type WitnessTypeList (ListElementType tt) :: [k]

Methods

toListElementWitness :: forall (t :: k0). ListElementType tt t -> ListElementType (WitnessTypeList (ListElementType tt)) t

fromListElementWitness :: forall (t :: k0). ListElementType (WitnessTypeList (ListElementType tt)) t -> ListElementType tt t

TestOrder (ListElementType tt :: k -> Type)

Defined in Data.Type.Witness.Specific.List.Element

Methods

testCompare :: forall (a :: k0) (b :: k0). ListElementType tt a -> ListElementType tt b -> WOrdering a b

Countable (ListElementType ('[] :: [k]) t)

Defined in Data.Type.Witness.Specific.List.Element

Methods

countPrevious :: ListElementType '[] t -> Maybe (ListElementType '[] t)

countMaybeNext :: Maybe (ListElementType '[] t) -> Maybe (ListElementType '[] t)

Empty (ListElementType ('[] :: [k]) t)

Defined in Data.Type.Witness.Specific.List.Element

Methods

never :: ListElementType '[] t -> a

Finite (ListElementType ('[] :: [k]) t)

Defined in Data.Type.Witness.Specific.List.Element

Methods

allValues :: [ListElementType '[] t]

assemble :: forall b f. Applicative f => (ListElementType '[] t -> f b) -> f (ListElementType '[] t -> b)

Searchable (ListElementType ('[] :: [k]) t)

Defined in Data.Type.Witness.Specific.List.Element

Methods

search :: (ListElementType '[] t -> Maybe b) -> Maybe b

Eq (ListElementType tt t)

Defined in Data.Type.Witness.Specific.List.Element

Methods

(==) :: ListElementType tt t -> ListElementType tt t -> Bool

(/=) :: ListElementType tt t -> ListElementType tt t -> Bool

type WitnessTypeList (ListElementType tt :: k -> Type)

Defined in Data.Type.Witness.General.ListElement

type WitnessTypeList (ListElementType tt :: k -> Type) = tt

pickListElement :: forall k (w :: k -> Type) (t :: k) (lt :: [k]). ListElementType lt t -> ListType w lt -> w t

lookUpListElement :: forall k (w :: k -> Type) (t :: k) (lt :: [k]). TestEquality w => w t -> ListType w lt -> Maybe (ListElementType lt t)

countListType :: ListType w lt -> ListType (ListElementType lt) lt

listElementTypeIndex :: Some (ListElementType lt) -> Some (Greater (ListLength lt))

indexListElementType :: ListType w lt -> Some (Greater (ListLength lt)) -> SomeFor w (ListElementType lt)