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]