Singleraeh.List

Documentation

data SList sa as where

Singleton list.

Constructors

SCons :: sa a -> SList sa as -> SList sa (a : as)

SNil :: SList sa '[]

Instances

Demotable sa => Demotable (SList sa :: [a] -> Type)

Defined in Singleraeh.List

Associated Types

type Demote (SList sa)

Methods

demote :: forall (k1 :: k). SList sa k1 -> Demote (SList sa)

type Demote (SList sa :: [a] -> Type)

Defined in Singleraeh.List

type Demote (SList sa :: [a] -> Type) = [Demote sa]

demoteSList :: forall da sa as. (forall a. sa a -> da) -> SList sa as -> [da]

type Reverse as = Reverse' '[] as

Reverse a type level list.

type family Reverse' (acc :: [k]) (as :: [k]) :: [k] where ...

Equations

Reverse' acc (a : as) = Reverse' (a : acc) as

Reverse' acc '[] = acc

sReverse :: SList sa as -> SList sa (Reverse as)

sReverse' :: SList sa acc -> SList sa as -> SList sa (Reverse' acc as)