Safe Haskell	None
Language	GHC2021

Data.Type.Witness.Specific.List.Element

Documentation

data ListElementType (kk :: [k]) (t :: k) where Source #

Constructors

FirstElementType :: forall {k} (t :: k) (tt :: [k]). ListElementType (t ': tt) t
RestElementType :: forall {k} (aa :: [k]) (t :: k) (a :: k). ListElementType aa t -> ListElementType (a ': aa) t

Instances

Instances details

TestEquality (ListElementType tt :: k -> Type) Source #

Instance details

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

Methods

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

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

Instance details

Defined in Data.Type.Witness.General.ListElement

Associated Types

type WitnessTypeList (ListElementType tt :: k -> Type)
Instance details Defined in Data.Type.Witness.General.ListElement type WitnessTypeList (ListElementType tt :: k -> Type) = tt

Methods

toListElementWitness :: forall (t :: k). ListElementType tt t -> ListElementType (WitnessTypeList (ListElementType tt)) t Source #

fromListElementWitness :: forall (t :: k). ListElementType (WitnessTypeList (ListElementType tt)) t -> ListElementType tt t Source #

TestOrder (ListElementType tt :: k -> Type) Source #

Instance details

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

Methods

testCompare :: forall (a :: k) (b :: k). ListElementType tt a -> ListElementType tt b -> WOrdering a b Source #

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

Instance details

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

Methods

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

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

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

Instance details

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

Methods

never :: ListElementType ('[] :: [k]) t -> a #

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

Instance details

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

Methods

allValues :: [ListElementType ('[] :: [k]) t] #

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

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

Instance details

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

Methods

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

Eq (ListElementType tt t) Source #

Instance details

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) Source #

Instance details

Defined in Data.Type.Witness.General.ListElement

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

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

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

countListType :: forall {k} (w :: k -> Type) (lt :: [k]). ListType w lt -> ListType (ListElementType lt) lt Source #

listElementTypeIndex :: forall {k} (lt :: [k]). Some (ListElementType lt) -> Some (Greater (ListLength lt)) Source #

indexListElementType :: forall {k} (w :: k -> Type) (lt :: [k]). ListType w lt -> Some (Greater (ListLength lt)) -> SomeFor w (ListElementType lt) Source #