#Emptiness Source

data Emptiness :: Type

#Empty Source

#NonEmpty Source

#SafeList Source

data SafeList t a

A list type that tracks the emptiness of the list.


#cons Source

cons :: forall t a. a -> SafeList t a -> SafeList NonEmpty a

#(:) Source

Operator alias for Data.List.Safe.cons (right-associative / precedence 6)

#nil Source

nil :: forall a. SafeList Empty a

#head Source

head :: forall a. SafeList NonEmpty a -> a

Get head of known-to-be-non-empty SafeList

#toNEL Source

toNEL :: forall a. SafeList NonEmpty a -> NonEmptyList a

Converts a known-to-be-non-empty SafeList into a NonEmptyList.

#toList Source

toList :: forall a t. SafeList t a -> List a

Converts a SafeList into a normal List.

#toUnfoldable Source

toUnfoldable :: forall a t f. Unfoldable f => SafeList t a -> f a

Converts a SafeList into some unfoldable structure.

#Leibniz Source

newtype Leibniz (a :: Emptiness) (b :: Emptiness)

Leibniz equality, specialised to Emptiness


#SafeListX Source

data SafeListX :: Type -> Type

A version of SafeList with the emptiness variable hidden.

#mkSafeListX Source

mkSafeListX :: forall a t. SafeList t a -> SafeListX a

#unSafeListX Source

unSafeListX :: forall r a. (forall t. SafeList t a -> r) -> SafeListX a -> r