Data.Singletons.Prelude.Maybe

data family Sing (a :: k)

type SMaybe

Singletons from Data.Maybe

maybe_

type family Maybe_ (a :: b) (a :: TyFun a b -> Type) (a :: Maybe a) :: b where ...

sMaybe_

type family IsJust (a :: Maybe a) :: Bool where ...

sIsJust

type family IsNothing (a :: Maybe a) :: Bool where ...

sIsNothing

type family FromJust (a :: Maybe a) :: a where ...

sFromJust

type family FromMaybe (a :: a) (a :: Maybe a) :: a where ...

sFromMaybe

type family ListToMaybe (a :: [a]) :: Maybe a where ...

sListToMaybe

type family MaybeToList (a :: Maybe a) :: [a] where ...

sMaybeToList

type family CatMaybes (a :: [Maybe a]) :: [a] where ...

sCatMaybes

type family MapMaybe (a :: TyFun a (Maybe b) -> Type) (a :: [a]) :: [b] where ...

sMapMaybe

Defunctionalization symbols

type NothingSym0

data JustSym0 l

type JustSym1 t

data Maybe_Sym0 l

data Maybe_Sym1 l l

data Maybe_Sym2 l l l

type Maybe_Sym3 t t t

data IsJustSym0 l

type IsJustSym1 t

data IsNothingSym0 l

type IsNothingSym1 t

data FromJustSym0 l

type FromJustSym1 t

data FromMaybeSym0 l

data FromMaybeSym1 l l

type FromMaybeSym2 t t

data ListToMaybeSym0 l

type ListToMaybeSym1 t

data MaybeToListSym0 l

type MaybeToListSym1 t

data CatMaybesSym0 l

type CatMaybesSym1 t

data MapMaybeSym0 l

data MapMaybeSym1 l l

type MapMaybeSym2 t t