Copyright	(C) 2013 Richard Eisenberg
License	BSD-style (see LICENSE)
Maintainer	Ryan Scott
Stability	experimental
Portability	non-portable
Safe Haskell	None
Language	Haskell2010

Data.Singletons

Contents

Main singleton definitions
Working with singletons
- Defunctionalization
- Defunctionalized singletons
Auxiliary functions
Defunctionalization symbols
Orphan instances

Description

This module exports the basic definitions to use singletons. For routine use, consider importing Prelude, which exports constructors for singletons based on types in the Prelude.

You may also want to read the original papers presenting this library, available at http://cs.brynmawr.edu/~rae/papers/2012/singletons/paper.pdf and http://cs.brynmawr.edu/~rae/papers/2014/promotion/promotion.pdf.

Synopsis

data family Sing :: k -> Type
(@@) :: forall k1 k2 (f :: k1 ~> k2) (t :: k1). Sing f -> Sing t -> Sing (f @@ t)
class SingI a where
- sing :: Sing a
class SingKind k where
- type Demote k = (r :: Type) | r -> k
- fromSing :: Sing (a :: k) -> Demote k
- toSing :: Demote k -> SomeSing k
type KindOf (a :: k) = k
type SameKind (a :: k) (b :: k) = (() :: Constraint)
data SingInstance (a :: k) where
- SingInstance :: SingI a => SingInstance a
data SomeSing k where
- SomeSing :: Sing (a :: k) -> SomeSing k
singInstance :: forall k (a :: k). Sing a -> SingInstance a
pattern Sing :: forall k (a :: k). () => SingI a => Sing a
withSingI :: Sing n -> (SingI n => r) -> r
withSomeSing :: forall k r. SingKind k => Demote k -> (forall (a :: k). Sing a -> r) -> r
pattern FromSing :: SingKind k => forall (a :: k). Sing a -> Demote k
singByProxy :: SingI a => proxy a -> Sing a
demote :: forall a. (SingKind (KindOf a), SingI a) => Demote (KindOf a)
singByProxy# :: SingI a => Proxy# a -> Sing a
withSing :: SingI a => (Sing a -> b) -> b
singThat :: forall k (a :: k). (SingKind k, SingI a) => (Demote k -> Bool) -> Maybe (Sing a)
data TyFun :: Type -> Type -> Type
type (~>) a b = TyFun a b -> Type
type TyCon1 = (TyCon :: (k1 -> k2) -> k1 ~> k2)
type TyCon2 = (TyCon :: (k1 -> k2 -> k3) -> k1 ~> (k2 ~> k3))
type TyCon3 = (TyCon :: (k1 -> k2 -> k3 -> k4) -> k1 ~> (k2 ~> (k3 ~> k4)))
type TyCon4 = (TyCon :: (k1 -> k2 -> k3 -> k4 -> k5) -> k1 ~> (k2 ~> (k3 ~> (k4 ~> k5))))
type TyCon5 = (TyCon :: (k1 -> k2 -> k3 -> k4 -> k5 -> k6) -> k1 ~> (k2 ~> (k3 ~> (k4 ~> (k5 ~> k6)))))
type TyCon6 = (TyCon :: (k1 -> k2 -> k3 -> k4 -> k5 -> k6 -> k7) -> k1 ~> (k2 ~> (k3 ~> (k4 ~> (k5 ~> (k6 ~> k7))))))
type TyCon7 = (TyCon :: (k1 -> k2 -> k3 -> k4 -> k5 -> k6 -> k7 -> k8) -> k1 ~> (k2 ~> (k3 ~> (k4 ~> (k5 ~> (k6 ~> (k7 ~> k8)))))))
type TyCon8 = (TyCon :: (k1 -> k2 -> k3 -> k4 -> k5 -> k6 -> k7 -> k8 -> k9) -> k1 ~> (k2 ~> (k3 ~> (k4 ~> (k5 ~> (k6 ~> (k7 ~> (k8 ~> k9))))))))
data family TyCon :: (k1 -> k2) -> unmatchable_fun
type family Apply (f :: k1 ~> k2) (x :: k1) :: k2
type (@@) a b = Apply a b
singFun1 :: forall f. SingFunction1 f -> Sing f
singFun2 :: forall f. SingFunction2 f -> Sing f
singFun3 :: forall f. SingFunction3 f -> Sing f
singFun4 :: forall f. SingFunction4 f -> Sing f
singFun5 :: forall f. SingFunction5 f -> Sing f
singFun6 :: forall f. SingFunction6 f -> Sing f
singFun7 :: forall f. SingFunction7 f -> Sing f
singFun8 :: forall f. SingFunction8 f -> Sing f
unSingFun1 :: forall f. Sing f -> SingFunction1 f
unSingFun2 :: forall f. Sing f -> SingFunction2 f
unSingFun3 :: forall f. Sing f -> SingFunction3 f
unSingFun4 :: forall f. Sing f -> SingFunction4 f
unSingFun5 :: forall f. Sing f -> SingFunction5 f
unSingFun6 :: forall f. Sing f -> SingFunction6 f
unSingFun7 :: forall f. Sing f -> SingFunction7 f
unSingFun8 :: forall f. Sing f -> SingFunction8 f
pattern SLambda2 :: forall f. SingFunction2 f -> Sing f
pattern SLambda3 :: forall f. SingFunction3 f -> Sing f
pattern SLambda4 :: forall f. SingFunction4 f -> Sing f
pattern SLambda5 :: forall f. SingFunction5 f -> Sing f
pattern SLambda6 :: forall f. SingFunction6 f -> Sing f
pattern SLambda7 :: forall f. SingFunction7 f -> Sing f
pattern SLambda8 :: forall f. SingFunction8 f -> Sing f
type SingFunction1 f = forall t. Sing t -> Sing (f @@ t)
type SingFunction2 f = forall t. Sing t -> SingFunction1 (f @@ t)
type SingFunction3 f = forall t. Sing t -> SingFunction2 (f @@ t)
type SingFunction4 f = forall t. Sing t -> SingFunction3 (f @@ t)
type SingFunction5 f = forall t. Sing t -> SingFunction4 (f @@ t)
type SingFunction6 f = forall t. Sing t -> SingFunction5 (f @@ t)
type SingFunction7 f = forall t. Sing t -> SingFunction6 (f @@ t)
type SingFunction8 f = forall t. Sing t -> SingFunction7 (f @@ t)
data Proxy (t :: k) :: forall k. k -> Type = Proxy
data DemoteSym0 :: (~>) Type Type
type DemoteSym1 (k6989586621679027556 :: Type) = Demote k6989586621679027556
data SameKindSym0 a6989586621679027562
data SameKindSym1 (a6989586621679027562 :: k6989586621679027561) b6989586621679027563
type SameKindSym2 (a6989586621679027562 :: k6989586621679027561) (b6989586621679027563 :: k6989586621679027561) = SameKind a6989586621679027562 b6989586621679027563
data KindOfSym0 a6989586621679027565
type KindOfSym1 (a6989586621679027565 :: k6989586621679027564) = KindOf a6989586621679027565
data (~>@#@$) a6989586621679025706
data (a6989586621679025706 :: Type) ~>@#@$$ b6989586621679025707
type (~>@#@$$$) (a6989586621679025706 :: Type) (b6989586621679025707 :: Type) = (~>) a6989586621679025706 b6989586621679025707
data ApplySym0 :: forall k16989586621679025703 k26989586621679025702. (~>) ((~>) k16989586621679025703 k26989586621679025702) ((~>) k16989586621679025703 k26989586621679025702)
data ApplySym1 (f6989586621679025704 :: (~>) k16989586621679025703 k26989586621679025702) :: (~>) k16989586621679025703 k26989586621679025702
type ApplySym2 (f6989586621679025704 :: (~>) k16989586621679025703 k26989586621679025702) (x6989586621679025705 :: k16989586621679025703) = Apply f6989586621679025704 x6989586621679025705
data (@@@#@$) a6989586621679025700
data (a6989586621679025700 :: (~>) k16989586621679031880 k6989586621679031878) @@@#@$$ b6989586621679025701
type (@@@#@$$$) (a6989586621679025700 :: (~>) k16989586621679031880 k6989586621679031878) (b6989586621679025701 :: k16989586621679031880) = (@@) a6989586621679025700 b6989586621679025701

Main singleton definitions

data family Sing :: k -> Type Source #

The singleton kind-indexed data family.

Instances

SDecide k => TestCoercion (Sing :: k -> Type) Source #
Instance details Defined in Data.Singletons.Decide Methods testCoercion :: Sing a -> Sing b -> Maybe (Coercion a b) #
SDecide k => TestEquality (Sing :: k -> Type) Source #
Instance details Defined in Data.Singletons.Decide Methods testEquality :: Sing a -> Sing b -> Maybe (a :~: b) #
Show (SSymbol s) Source #
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> SSymbol s -> ShowS # show :: SSymbol s -> String # showList :: [SSymbol s] -> ShowS #
Show (SNat n) Source #
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> SNat n -> ShowS # show :: SNat n -> String # showList :: [SNat n] -> ShowS #
Eq (Sing a) Source #
Instance details Defined in Data.Singletons.TypeRepTYPE Methods (==) :: Sing a -> Sing a -> Bool # (/=) :: Sing a -> Sing a -> Bool #
Ord (Sing a) Source #
Instance details Defined in Data.Singletons.TypeRepTYPE Methods compare :: Sing a -> Sing a -> Ordering # (<) :: Sing a -> Sing a -> Bool # (<=) :: Sing a -> Sing a -> Bool # (>) :: Sing a -> Sing a -> Bool # (>=) :: Sing a -> Sing a -> Bool # max :: Sing a -> Sing a -> Sing a # min :: Sing a -> Sing a -> Sing a #
Show (Sing z) Source #
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> Sing z -> ShowS # show :: Sing z -> String # showList :: [Sing z] -> ShowS #
(ShowSing a, ShowSing [a]) => Show (Sing z) Source #
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> Sing z -> ShowS # show :: Sing z -> String # showList :: [Sing z] -> ShowS #
ShowSing a => Show (Sing z) Source #
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> Sing z -> ShowS # show :: Sing z -> String # showList :: [Sing z] -> ShowS #
Show (Sing z) Source #
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> Sing z -> ShowS # show :: Sing z -> String # showList :: [Sing z] -> ShowS #
(ShowSing a, ShowSing b) => Show (Sing z) Source #
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> Sing z -> ShowS # show :: Sing z -> String # showList :: [Sing z] -> ShowS #
Show (Sing a) Source #
Instance details Defined in Data.Singletons.TypeRepTYPE Methods showsPrec :: Int -> Sing a -> ShowS # show :: Sing a -> String # showList :: [Sing a] -> ShowS #
Show (Sing z) Source #
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> Sing z -> ShowS # show :: Sing z -> String # showList :: [Sing z] -> ShowS #
(ShowSing a, ShowSing b) => Show (Sing z) Source #
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> Sing z -> ShowS # show :: Sing z -> String # showList :: [Sing z] -> ShowS #
(ShowSing a, ShowSing b, ShowSing c) => Show (Sing z) Source #
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> Sing z -> ShowS # show :: Sing z -> String # showList :: [Sing z] -> ShowS #
(ShowSing a, ShowSing b, ShowSing c, ShowSing d) => Show (Sing z) Source #
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> Sing z -> ShowS # show :: Sing z -> String # showList :: [Sing z] -> ShowS #
(ShowSing a, ShowSing b, ShowSing c, ShowSing d, ShowSing e) => Show (Sing z) Source #
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> Sing z -> ShowS # show :: Sing z -> String # showList :: [Sing z] -> ShowS #
(ShowSing a, ShowSing b, ShowSing c, ShowSing d, ShowSing e, ShowSing f) => Show (Sing z) Source #
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> Sing z -> ShowS # show :: Sing z -> String # showList :: [Sing z] -> ShowS #
(ShowSing a, ShowSing b, ShowSing c, ShowSing d, ShowSing e, ShowSing f, ShowSing g) => Show (Sing z) Source #
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> Sing z -> ShowS # show :: Sing z -> String # showList :: [Sing z] -> ShowS #
Show (Sing z) Source #
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> Sing z -> ShowS # show :: Sing z -> String # showList :: [Sing z] -> ShowS #
ShowSing a => Show (Sing z) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods showsPrec :: Int -> Sing z -> ShowS # show :: Sing z -> String # showList :: [Sing z] -> ShowS #
ShowSing a => Show (Sing z) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods showsPrec :: Int -> Sing z -> ShowS # show :: Sing z -> String # showList :: [Sing z] -> ShowS #
(ShowSing a, ShowSing b) => Show (Sing z) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods showsPrec :: Int -> Sing z -> ShowS # show :: Sing z -> String # showList :: [Sing z] -> ShowS #
ShowSing a => Show (Sing z) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods showsPrec :: Int -> Sing z -> ShowS # show :: Sing z -> String # showList :: [Sing z] -> ShowS #
ShowSing a => Show (Sing z) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods showsPrec :: Int -> Sing z -> ShowS # show :: Sing z -> String # showList :: [Sing z] -> ShowS #
ShowSing m => Show (Sing z) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods showsPrec :: Int -> Sing z -> ShowS # show :: Sing z -> String # showList :: [Sing z] -> ShowS #
ShowSing (Maybe a) => Show (Sing z) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods showsPrec :: Int -> Sing z -> ShowS # show :: Sing z -> String # showList :: [Sing z] -> ShowS #
ShowSing a => Show (Sing z) Source #
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> Sing z -> ShowS # show :: Sing z -> String # showList :: [Sing z] -> ShowS #
ShowSing (Maybe a) => Show (Sing z) Source #
Instance details Defined in Data.Singletons.Prelude.Monoid Methods showsPrec :: Int -> Sing z -> ShowS # show :: Sing z -> String # showList :: [Sing z] -> ShowS #
ShowSing (Maybe a) => Show (Sing z) Source #
Instance details Defined in Data.Singletons.Prelude.Monoid Methods showsPrec :: Int -> Sing z -> ShowS # show :: Sing z -> String # showList :: [Sing z] -> ShowS #
ShowSing a => Show (Sing z) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods showsPrec :: Int -> Sing z -> ShowS # show :: Sing z -> String # showList :: [Sing z] -> ShowS #
ShowSing Bool => Show (Sing z) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods showsPrec :: Int -> Sing z -> ShowS # show :: Sing z -> String # showList :: [Sing z] -> ShowS #
ShowSing Bool => Show (Sing z) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods showsPrec :: Int -> Sing z -> ShowS # show :: Sing z -> String # showList :: [Sing z] -> ShowS #
ShowSing a => Show (Sing z) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods showsPrec :: Int -> Sing z -> ShowS # show :: Sing z -> String # showList :: [Sing z] -> ShowS #
ShowSing a => Show (Sing z) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods showsPrec :: Int -> Sing z -> ShowS # show :: Sing z -> String # showList :: [Sing z] -> ShowS #
(ShowSing a, ShowSing [a]) => Show (Sing z) Source #
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> Sing z -> ShowS # show :: Sing z -> String # showList :: [Sing z] -> ShowS #
data Sing (a :: Bool) Source #
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (a :: Bool) where SFalse :: forall (a :: Bool). Sing False STrue :: forall (a :: Bool). Sing True
data Sing (a :: Ordering) Source #
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (a :: Ordering) where SLT :: forall (a :: Ordering). Sing LT SEQ :: forall (a :: Ordering). Sing EQ SGT :: forall (a :: Ordering). Sing GT
data Sing (n :: Nat) Source #
Instance details Defined in Data.Singletons.TypeLits.Internal data Sing (n :: Nat) where SNat :: forall (n :: Nat). KnownNat n => Sing n
data Sing (n :: Symbol) Source #
Instance details Defined in Data.Singletons.TypeLits.Internal data Sing (n :: Symbol) where SSym :: forall (n :: Symbol). KnownSymbol n => Sing n
data Sing (a :: ()) Source #
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (a :: ()) where STuple0 :: forall (a :: ()). Sing ()
data Sing (a :: Void) Source #
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (a :: Void)
data Sing (a :: All) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal data Sing (a :: All) where SAll :: forall (a :: All) (n :: Bool). {..} -> Sing (All n)
data Sing (a :: Any) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal data Sing (a :: Any) where SAny :: forall (a :: Any) (n :: Bool). {..} -> Sing (Any n)
data Sing (a :: PErrorMessage) Source #
Instance details Defined in Data.Singletons.TypeError data Sing (a :: PErrorMessage) where SText :: forall (a :: PErrorMessage) (t :: Symbol). Sing t -> Sing (Text t) SShowType :: forall (a :: PErrorMessage) t (ty :: t). Sing ty -> Sing (ShowType ty :: ErrorMessage' Symbol) (:%<>:) :: forall (a :: PErrorMessage) (e1 :: ErrorMessage' Symbol) (e2 :: ErrorMessage' Symbol). Sing e1 -> Sing e2 -> Sing (e1 :<>: e2) (:%$$:) :: forall (a :: PErrorMessage) (e1 :: ErrorMessage' Symbol) (e2 :: ErrorMessage' Symbol). Sing e1 -> Sing e2 -> Sing (e1 :$$: e2)
data Sing (b :: [a]) Source #
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (b :: [a]) where SNil :: forall k (b :: [k]). Sing ([] :: [k]) SCons :: forall a (b :: [a]) (n :: a) (n :: [a]). Sing n -> Sing n -> Sing (n ': n)
data Sing (b :: Maybe a) Source #
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (b :: Maybe a) where SNothing :: forall a (b :: Maybe a). Sing (Nothing :: Maybe a) SJust :: forall a (b :: Maybe a) (n :: a). Sing n -> Sing (Just n)
data Sing (a :: TYPE rep) Source #	A choice of singleton for the kind `TYPE rep` (for some `RuntimeRep` `rep`), an instantiation of which is the famous kind `Type`. Conceivably, one could generalize this instance to `Sing :: k -> Type` for any kind `k`, and remove all other `Sing` instances. We don't adopt this design, however, since it is far more convenient in practice to work with explicit singleton values than `TypeRep`s (for instance, `TypeRep`s are more difficult to pattern match on, and require extra runtime checks). We cannot produce explicit singleton values for everything in `TYPE rep`, however, since it is an open kind, so we reach for `TypeRep` in this one particular case.
Instance details Defined in Data.Singletons.TypeRepTYPE data Sing (a :: TYPE rep) = STypeRep (TypeRep a)
data Sing (b :: Min a) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal data Sing (b :: Min a) where SMin :: forall a (b :: Min a) (n :: a). {..} -> Sing (Min n)
data Sing (b :: Max a) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal data Sing (b :: Max a) where SMax :: forall a (b :: Max a) (n :: a). {..} -> Sing (Max n)
data Sing (b :: First a) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal data Sing (b :: First a) where SFirst :: forall a (b :: First a) (n :: a). {..} -> Sing (First n)
data Sing (b :: Last a) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal data Sing (b :: Last a) where SLast :: forall a (b :: Last a) (n :: a). {..} -> Sing (Last n)
data Sing (a :: WrappedMonoid m) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal data Sing (a :: WrappedMonoid m) where SWrapMonoid :: forall m (a :: WrappedMonoid m) (n :: m). {..} -> Sing (WrapMonoid n)
data Sing (b :: Option a) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal data Sing (b :: Option a) where SOption :: forall a (b :: Option a) (n :: Maybe a). {..} -> Sing (Option n)
data Sing (b :: Identity a) Source #
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (b :: Identity a) where SIdentity :: forall a (b :: Identity a) (n :: a). {..} -> Sing (Identity n)
data Sing (b :: First a) Source #
Instance details Defined in Data.Singletons.Prelude.Monoid data Sing (b :: First a) where SFirst :: forall a (b :: First a) (n :: Maybe a). {..} -> Sing (First n)
data Sing (b :: Last a) Source #
Instance details Defined in Data.Singletons.Prelude.Monoid data Sing (b :: Last a) where SLast :: forall a (b :: Last a) (n :: Maybe a). {..} -> Sing (Last n)
data Sing (b :: Dual a) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal data Sing (b :: Dual a) where SDual :: forall a (b :: Dual a) (n :: a). {..} -> Sing (Dual n)
data Sing (b :: Sum a) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal data Sing (b :: Sum a) where SSum :: forall a (b :: Sum a) (n :: a). {..} -> Sing (Sum n)
data Sing (b :: Product a) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal data Sing (b :: Product a) where SProduct :: forall a (b :: Product a) (n :: a). {..} -> Sing (Product n)
data Sing (b :: Down a) Source #
Instance details Defined in Data.Singletons.Prelude.Ord data Sing (b :: Down a) where SDown :: forall a (b :: Down a) (n :: a). Sing n -> Sing (Down n)
data Sing (b :: NonEmpty a) Source #
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (b :: NonEmpty a) where (:%\|) :: forall a (b :: NonEmpty a) (n :: a) (n :: [a]). Sing n -> Sing n -> Sing (n :\| n)
data Sing (c :: Either a b) Source #
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (c :: Either a b) where SLeft :: forall a b (c :: Either a b) (n :: a). Sing n -> Sing (Left n :: Either a b) SRight :: forall a b (c :: Either a b) (n :: b). Sing n -> Sing (Right n :: Either a b)
data Sing (c :: (a, b)) Source #
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (c :: (a, b)) where STuple2 :: forall a b (c :: (a, b)) (n :: a) (n :: b). Sing n -> Sing n -> Sing ((,) n n)
data Sing (c :: Arg a b) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup data Sing (c :: Arg a b) where SArg :: forall a b (c :: Arg a b) (n :: a) (n :: b). Sing n -> Sing n -> Sing (Arg n n)
data Sing (f :: k1 ~> k2) Source #
Instance details Defined in Data.Singletons.Internal data Sing (f :: k1 ~> k2) = SLambda { applySing :: forall (t :: k1). Sing t -> Sing (f @@ t) }
data Sing (d :: (a, b, c)) Source #
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (d :: (a, b, c)) where STuple3 :: forall a b c (d :: (a, b, c)) (n :: a) (n :: b) (n :: c). Sing n -> Sing n -> Sing n -> Sing ((,,) n n n)
data Sing (c :: Const a b) Source #
Instance details Defined in Data.Singletons.Prelude.Const data Sing (c :: Const a b) where SConst :: forall k a (b :: k) (c :: Const a b) (a :: a). {..} -> Sing (Const a :: Const a b)
data Sing (e :: (a, b, c, d)) Source #
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (e :: (a, b, c, d)) where STuple4 :: forall a b c d (e :: (a, b, c, d)) (n :: a) (n :: b) (n :: c) (n :: d). Sing n -> Sing n -> Sing n -> Sing n -> Sing ((,,,) n n n n)
data Sing (f :: (a, b, c, d, e)) Source #
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (f :: (a, b, c, d, e)) where STuple5 :: forall a b c d e (f :: (a, b, c, d, e)) (n :: a) (n :: b) (n :: c) (n :: d) (n :: e). Sing n -> Sing n -> Sing n -> Sing n -> Sing n -> Sing ((,,,,) n n n n n)
data Sing (g :: (a, b, c, d, e, f)) Source #
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (g :: (a, b, c, d, e, f)) where STuple6 :: forall a b c d e f (g :: (a, b, c, d, e, f)) (n :: a) (n :: b) (n :: c) (n :: d) (n :: e) (n :: f). Sing n -> Sing n -> Sing n -> Sing n -> Sing n -> Sing n -> Sing ((,,,,,) n n n n n n)
data Sing (h :: (a, b, c, d, e, f, g)) Source #
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (h :: (a, b, c, d, e, f, g)) where STuple7 :: forall a b c d e f g (h :: (a, b, c, d, e, f, g)) (n :: a) (n :: b) (n :: c) (n :: d) (n :: e) (n :: f) (n :: g). Sing n -> Sing n -> Sing n -> Sing n -> Sing n -> Sing n -> Sing n -> Sing ((,,,,,,) n n n n n n n)

(@@) :: forall k1 k2 (f :: k1 ~> k2) (t :: k1). Sing f -> Sing t -> Sing (f @@ t) infixl 9 Source #

An infix synonym for applySing

class SingI a where Source #

A SingI constraint is essentially an implicitly-passed singleton. If you need to satisfy this constraint with an explicit singleton, please see withSingI or the Sing pattern synonym.

Methods

sing :: Sing a Source #

Produce the singleton explicitly. You will likely need the ScopedTypeVariables extension to use this method the way you want.

Instances

SingI False Source #
Instance details Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing False Source #
SingI True Source #
Instance details Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing True Source #
SingI LT Source #
Instance details Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing LT Source #
SingI EQ Source #
Instance details Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing EQ Source #
SingI GT Source #
Instance details Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing GT Source #
KnownNat n => SingI (n :: Nat) Source #
Instance details Defined in Data.Singletons.TypeLits.Internal Methods sing :: Sing n Source #
KnownSymbol n => SingI (n :: Symbol) Source #
Instance details Defined in Data.Singletons.TypeLits.Internal Methods sing :: Sing n Source #
SingI () Source #
Instance details Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing () Source #
SingI n => SingI (All n :: All) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Methods sing :: Sing (All0 n) Source #
SingI n => SingI (Any n :: Any) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Methods sing :: Sing (Any0 n) Source #
SingI t => SingI (Text t :: ErrorMessage' Symbol) Source #
Instance details Defined in Data.Singletons.TypeError Methods sing :: Sing (Text t) Source #
SingI ty => SingI (ShowType ty :: ErrorMessage' Symbol) Source #
Instance details Defined in Data.Singletons.TypeError Methods sing :: Sing (ShowType ty) Source #
(SingI e1, SingI e2) => SingI (e1 :<>: e2 :: ErrorMessage' Symbol) Source #
Instance details Defined in Data.Singletons.TypeError Methods sing :: Sing (e1 :<>: e2) Source #
(SingI e1, SingI e2) => SingI (e1 :$$: e2 :: ErrorMessage' Symbol) Source #
Instance details Defined in Data.Singletons.TypeError Methods sing :: Sing (e1 :$$: e2) Source #
Typeable a => SingI (a :: TYPE rep) Source #
Instance details Defined in Data.Singletons.TypeRepTYPE Methods sing :: Sing a Source #
SingI ([] :: [k]) Source #
Instance details Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing [] Source #
SingI (Nothing :: Maybe a) Source #
Instance details Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing Nothing Source #
SingI n => SingI (Just n :: Maybe a) Source #
Instance details Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing (Just n) Source #
SingI n => SingI (Min n :: Min a) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Methods sing :: Sing (Min0 n) Source #
SingI n => SingI (Max n :: Max a) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Methods sing :: Sing (Max0 n) Source #
SingI n => SingI (First n :: First a) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Methods sing :: Sing (First0 n) Source #
SingI n => SingI (Last n :: Last a) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Methods sing :: Sing (Last0 n) Source #
SingI n => SingI (WrapMonoid n :: WrappedMonoid m) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Methods sing :: Sing (WrapMonoid n) Source #
SingI n => SingI (Option n :: Option a) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Methods sing :: Sing (Option0 n) Source #
SingI n => SingI (Identity n :: Identity a) Source #
Instance details Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing (Identity0 n) Source #
SingI n => SingI (First n :: First a) Source #
Instance details Defined in Data.Singletons.Prelude.Monoid Methods sing :: Sing (First0 n) Source #
SingI n => SingI (Last n :: Last a) Source #
Instance details Defined in Data.Singletons.Prelude.Monoid Methods sing :: Sing (Last0 n) Source #
SingI n => SingI (Dual n :: Dual a) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Methods sing :: Sing (Dual0 n) Source #
SingI n => SingI (Sum n :: Sum a) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Methods sing :: Sing (Sum0 n) Source #
SingI n => SingI (Product n :: Product a) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Methods sing :: Sing (Product0 n) Source #
SingI n => SingI (Down n :: Down a) Source #
Instance details Defined in Data.Singletons.Prelude.Ord Methods sing :: Sing (Down0 n) Source #
(SingI n1, SingI n2) => SingI (n1 ': n2 :: [a]) Source #
Instance details Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing (n1 ': n2) Source #
(SingI n1, SingI n2) => SingI (n1 :\| n2 :: NonEmpty a) Source #
Instance details Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing (n1 :\| n2) Source #
SingI NotSym0 Source #
Instance details Defined in Data.Singletons.Prelude.Bool Methods sing :: Sing NotSym0 Source #
SingI (&&@#@$) Source #
Instance details Defined in Data.Singletons.Prelude.Bool Methods sing :: Sing (&&@#@$) Source #
SingI (\|\|@#@$) Source #
Instance details Defined in Data.Singletons.Prelude.Bool Methods sing :: Sing (\|\|@#@$) Source #
SingI Log2Sym0 Source #
Instance details Defined in Data.Singletons.TypeLits Methods sing :: Sing Log2Sym0 Source #
SingI (<=?@#@$) Source #
Instance details Defined in Data.Singletons.TypeLits.Internal Methods sing :: Sing (<=?@#@$) Source #
SingI (^@#@$) Source #
Instance details Defined in Data.Singletons.TypeLits.Internal Methods sing :: Sing (^@#@$) Source #
SingI DivSym0 Source #
Instance details Defined in Data.Singletons.TypeLits Methods sing :: Sing DivSym0 Source #
SingI ModSym0 Source #
Instance details Defined in Data.Singletons.TypeLits Methods sing :: Sing ModSym0 Source #
SingI AllSym0 Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Methods sing :: Sing AllSym0 Source #
SingI AnySym0 Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Methods sing :: Sing AnySym0 Source #
SingI ShowParenSym0 Source #
Instance details Defined in Data.Singletons.Prelude.Show Methods sing :: Sing ShowParenSym0 Source #
SingI UnlinesSym0 Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing UnlinesSym0 Source #
SingI UnwordsSym0 Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing UnwordsSym0 Source #
SingI ThenCmpSym0 Source #
Instance details Defined in Data.Singletons.Prelude.Ord Methods sing :: Sing ThenCmpSym0 Source #
SingI ShowCommaSpaceSym0 Source #
Instance details Defined in Data.Singletons.Prelude.Show Methods sing :: Sing ShowCommaSpaceSym0 Source #
SingI ShowSpaceSym0 Source #
Instance details Defined in Data.Singletons.Prelude.Show Methods sing :: Sing ShowSpaceSym0 Source #
SingI ShowCharSym0 Source #
Instance details Defined in Data.Singletons.Prelude.Show Methods sing :: Sing ShowCharSym0 Source #
SingI ShowStringSym0 Source #
Instance details Defined in Data.Singletons.Prelude.Show Methods sing :: Sing ShowStringSym0 Source #
SingI XorSym0 Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods sing :: Sing XorSym0 Source #
SingI x => SingI ((&&@#@$$) x :: TyFun Bool Bool -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Bool Methods sing :: Sing ((&&@#@$$) x) Source #
SingI x => SingI ((\|\|@#@$$) x :: TyFun Bool Bool -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Bool Methods sing :: Sing ((\|\|@#@$$) x) Source #
SingI x => SingI ((<=?@#@$$) x :: TyFun Nat Bool -> Type) Source #
Instance details Defined in Data.Singletons.TypeLits.Internal Methods sing :: Sing ((<=?@#@$$) x) Source #
SingI x => SingI ((^@#@$$) x :: TyFun Nat Nat -> Type) Source #
Instance details Defined in Data.Singletons.TypeLits.Internal Methods sing :: Sing ((^@#@$$) x) Source #
SingI x => SingI (DivSym1 x :: TyFun Nat Nat -> Type) Source #
Instance details Defined in Data.Singletons.TypeLits Methods sing :: Sing (DivSym1 x) Source #
SingI x => SingI (ModSym1 x :: TyFun Nat Nat -> Type) Source #
Instance details Defined in Data.Singletons.TypeLits Methods sing :: Sing (ModSym1 x) Source #
SingI (TypeErrorSym0 :: TyFun PErrorMessage b6989586621681244485 -> Type) Source #
Instance details Defined in Data.Singletons.TypeError Methods sing :: Sing TypeErrorSym0 Source #
SingI (JustSym0 :: TyFun a (Maybe a) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing JustSym0 Source #
SingI ((:@#@$) :: TyFun a ([a] ~> [a]) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing (:@#@$) Source #
SAlternative f => SingI (GuardSym0 :: TyFun Bool (f ()) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing GuardSym0 Source #
SApplicative f => SingI (WhenSym0 :: TyFun Bool (f () ~> f ()) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing WhenSym0 Source #
SApplicative f => SingI (UnlessSym0 :: TyFun Bool (f () ~> f ()) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Monad Methods sing :: Sing UnlessSym0 Source #
SingI (TransposeSym0 :: TyFun [[a]] [[a]] -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing TransposeSym0 Source #
SingI (CatMaybesSym0 :: TyFun [Maybe a] [a] -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Maybe Methods sing :: Sing CatMaybesSym0 Source #
SingI (ListToMaybeSym0 :: TyFun [a] (Maybe a) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Maybe Methods sing :: Sing ListToMaybeSym0 Source #
SingI ((++@#@$) :: TyFun [a] ([a] ~> [a]) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Base Methods sing :: Sing (++@#@$) Source #
SEq a => SingI (UnionSym0 :: TyFun [a] ([a] ~> [a]) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing UnionSym0 Source #
SEq a => SingI (NubSym0 :: TyFun [a] [a] -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing NubSym0 Source #
SingI ((!!@#@$) :: TyFun [a] (Nat ~> a) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (!!@#@$) Source #
SOrd a => SingI (SortSym0 :: TyFun [a] [a] -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing SortSym0 Source #
SEq a => SingI (GroupSym0 :: TyFun [a] [[a]] -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing GroupSym0 Source #
SEq a => SingI (IntersectSym0 :: TyFun [a] ([a] ~> [a]) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing IntersectSym0 Source #
SEq a => SingI ((\\@#@$) :: TyFun [a] ([a] ~> [a]) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (\\@#@$) Source #
SEq a => SingI (IsInfixOfSym0 :: TyFun [a] ([a] ~> Bool) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing IsInfixOfSym0 Source #
SEq a => SingI (IsSuffixOfSym0 :: TyFun [a] ([a] ~> Bool) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing IsSuffixOfSym0 Source #
SEq a => SingI (IsPrefixOfSym0 :: TyFun [a] ([a] ~> Bool) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing IsPrefixOfSym0 Source #
SingI (TailsSym0 :: TyFun [a] [[a]] -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing TailsSym0 Source #
SingI (InitsSym0 :: TyFun [a] [[a]] -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing InitsSym0 Source #
SingI (PermutationsSym0 :: TyFun [a] [[a]] -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing PermutationsSym0 Source #
SingI (SubsequencesSym0 :: TyFun [a] [[a]] -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing SubsequencesSym0 Source #
SingI (IntercalateSym0 :: TyFun [a] ([[a]] ~> [a]) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing IntercalateSym0 Source #
SingI (ReverseSym0 :: TyFun [a] [a] -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing ReverseSym0 Source #
SingI (InitSym0 :: TyFun [a] [a] -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing InitSym0 Source #
SingI (TailSym0 :: TyFun [a] [a] -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing TailSym0 Source #
SingI (LastSym0 :: TyFun [a] a -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing LastSym0 Source #
SingI (HeadSym0 :: TyFun [a] a -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing HeadSym0 Source #
SShow a => SingI (ShowListSym0 :: TyFun [a] (Symbol ~> Symbol) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Show Methods sing :: Sing ShowListSym0 Source #
SMonoid a => SingI (MconcatSym0 :: TyFun [a] a -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Monoid Methods sing :: Sing MconcatSym0 Source #
SEq a => SingI (IsPrefixOfSym0 :: TyFun [a] (NonEmpty a ~> Bool) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods sing :: Sing IsPrefixOfSym0 Source #
SEq a => SingI (GroupSym0 :: TyFun [a] [NonEmpty a] -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods sing :: Sing GroupSym0 Source #
SingI (TailsSym0 :: TyFun [a] (NonEmpty [a]) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods sing :: Sing TailsSym0 Source #
SingI (InitsSym0 :: TyFun [a] (NonEmpty [a]) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods sing :: Sing InitsSym0 Source #
SingI (FromListSym0 :: TyFun [a] (NonEmpty a) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods sing :: Sing FromListSym0 Source #
SingI (NonEmpty_Sym0 :: TyFun [a] (Maybe (NonEmpty a)) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods sing :: Sing NonEmpty_Sym0 Source #
SingI (OptionSym0 :: TyFun (Maybe a) (Option a) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Methods sing :: Sing OptionSym0 Source #
SingI (LastSym0 :: TyFun (Maybe a) (Last a) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Monoid Methods sing :: Sing LastSym0 Source #
SingI (FirstSym0 :: TyFun (Maybe a) (First a) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Monoid Methods sing :: Sing FirstSym0 Source #
SingI (MaybeToListSym0 :: TyFun (Maybe a) [a] -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Maybe Methods sing :: Sing MaybeToListSym0 Source #
SingI (FromJustSym0 :: TyFun (Maybe a) a -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Maybe Methods sing :: Sing FromJustSym0 Source #
SingI (IsNothingSym0 :: TyFun (Maybe a) Bool -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Maybe Methods sing :: Sing IsNothingSym0 Source #
SingI (IsJustSym0 :: TyFun (Maybe a) Bool -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Maybe Methods sing :: Sing IsJustSym0 Source #
SingI d => SingI (ThenCmpSym1 d :: TyFun Ordering Ordering -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Ord Methods sing :: Sing (ThenCmpSym1 d) Source #
SNum a => SingI (FromIntegerSym0 :: TyFun Nat a -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Num Methods sing :: Sing FromIntegerSym0 Source #
SEnum a => SingI (ToEnumSym0 :: TyFun Nat a -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Enum Methods sing :: Sing ToEnumSym0 Source #
SingI (SplitAtSym0 :: TyFun Nat ([a] ~> ([a], [a])) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing SplitAtSym0 Source #
SingI (DropSym0 :: TyFun Nat ([a] ~> [a]) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing DropSym0 Source #
SingI (TakeSym0 :: TyFun Nat ([a] ~> [a]) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing TakeSym0 Source #
SingI (ReplicateSym0 :: TyFun Nat (a ~> [a]) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing ReplicateSym0 Source #
SShow a => SingI (ShowsPrecSym0 :: TyFun Nat (a ~> (Symbol ~> Symbol)) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Show Methods sing :: Sing ShowsPrecSym0 Source #
SingI (SplitAtSym0 :: TyFun Nat (NonEmpty a ~> ([a], [a])) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods sing :: Sing SplitAtSym0 Source #
SingI (DropSym0 :: TyFun Nat (NonEmpty a ~> [a]) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods sing :: Sing DropSym0 Source #
SingI (TakeSym0 :: TyFun Nat (NonEmpty a ~> [a]) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods sing :: Sing TakeSym0 Source #
SingI d => SingI (ShowCharSym1 d :: TyFun Symbol Symbol -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Show Methods sing :: Sing (ShowCharSym1 d) Source #
SingI d => SingI (ShowStringSym1 d :: TyFun Symbol Symbol -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Show Methods sing :: Sing (ShowStringSym1 d) Source #
SIsString a => SingI (FromStringSym0 :: TyFun Symbol a -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.IsString Methods sing :: Sing FromStringSym0 Source #
SingI (TextSym0 :: TyFun Symbol (ErrorMessage' Symbol) -> Type) Source #
Instance details Defined in Data.Singletons.TypeError Methods sing :: Sing TextSym0 Source #
SingI (MinSym0 :: TyFun a (Min a) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Methods sing :: Sing MinSym0 Source #
SingI (MaxSym0 :: TyFun a (Max a) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Methods sing :: Sing MaxSym0 Source #
SingI (FirstSym0 :: TyFun a (First a) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Methods sing :: Sing FirstSym0 Source #
SingI (LastSym0 :: TyFun a (Last a) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Methods sing :: Sing LastSym0 Source #
SingI (WrapMonoidSym0 :: TyFun m (WrappedMonoid m) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Methods sing :: Sing WrapMonoidSym0 Source #
SingI ((:\|@#@$) :: TyFun a ([a] ~> NonEmpty a) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing (:\|@#@$) Source #
SingI (SumSym0 :: TyFun a (Sum a) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Methods sing :: Sing SumSym0 Source #
SingI (ProductSym0 :: TyFun a (Product a) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Methods sing :: Sing ProductSym0 Source #
SingI (DualSym0 :: TyFun a (Dual a) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Methods sing :: Sing DualSym0 Source #
SingI (IdentitySym0 :: TyFun a (Identity a) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing IdentitySym0 Source #
SingI (DownSym0 :: TyFun a (Down a) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Ord Methods sing :: Sing DownSym0 Source #
SingI (Bool_Sym0 :: TyFun a (a ~> (Bool ~> a)) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Bool Methods sing :: Sing Bool_Sym0 Source #
SEq a => SingI ((/=@#@$) :: TyFun a (a ~> Bool) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Eq Methods sing :: Sing (/=@#@$) Source #
SEq a => SingI ((==@#@$) :: TyFun a (a ~> Bool) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Eq Methods sing :: Sing (==@#@$) Source #
SOrd a => SingI ((>=@#@$) :: TyFun a (a ~> Bool) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Ord Methods sing :: Sing (>=@#@$) Source #
SOrd a => SingI ((>@#@$) :: TyFun a (a ~> Bool) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Ord Methods sing :: Sing (>@#@$) Source #
SOrd a => SingI ((<=@#@$) :: TyFun a (a ~> Bool) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Ord Methods sing :: Sing (<=@#@$) Source #
SOrd a => SingI ((<@#@$) :: TyFun a (a ~> Bool) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Ord Methods sing :: Sing (<@#@$) Source #
SOrd a => SingI (CompareSym0 :: TyFun a (a ~> Ordering) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Ord Methods sing :: Sing CompareSym0 Source #
SOrd a => SingI (MinSym0 :: TyFun a (a ~> a) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Ord Methods sing :: Sing MinSym0 Source #
SOrd a => SingI (MaxSym0 :: TyFun a (a ~> a) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Ord Methods sing :: Sing MaxSym0 Source #
SingI (FromMaybeSym0 :: TyFun a (Maybe a ~> a) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Maybe Methods sing :: Sing FromMaybeSym0 Source #
SNum a => SingI (SignumSym0 :: TyFun a a -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Num Methods sing :: Sing SignumSym0 Source #
SNum a => SingI (AbsSym0 :: TyFun a a -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Num Methods sing :: Sing AbsSym0 Source #
SNum a => SingI (NegateSym0 :: TyFun a a -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Num Methods sing :: Sing NegateSym0 Source #
SNum a => SingI ((*@#@$) :: TyFun a (a ~> a) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Num Methods sing :: Sing (*@#@$) Source #
SNum a => SingI ((-@#@$) :: TyFun a (a ~> a) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Num Methods sing :: Sing (-@#@$) Source #
SNum a => SingI ((+@#@$) :: TyFun a (a ~> a) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Num Methods sing :: Sing (+@#@$) Source #
SNum a => SingI (SubtractSym0 :: TyFun a (a ~> a) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Num Methods sing :: Sing SubtractSym0 Source #
SingI (AsTypeOfSym0 :: TyFun a (a ~> a) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Base Methods sing :: Sing AsTypeOfSym0 Source #
SingI (IdSym0 :: TyFun a a -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Base Methods sing :: Sing IdSym0 Source #
SEnum a => SingI (FromEnumSym0 :: TyFun a Nat -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Enum Methods sing :: Sing FromEnumSym0 Source #
SEnum a => SingI (PredSym0 :: TyFun a a -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Enum Methods sing :: Sing PredSym0 Source #
SEnum a => SingI (SuccSym0 :: TyFun a a -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Enum Methods sing :: Sing SuccSym0 Source #
SEnum a => SingI (EnumFromToSym0 :: TyFun a (a ~> [a]) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Enum Methods sing :: Sing EnumFromToSym0 Source #
SEnum a => SingI (EnumFromThenToSym0 :: TyFun a (a ~> (a ~> [a])) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Enum Methods sing :: Sing EnumFromThenToSym0 Source #
SSemigroup a => SingI ((<>@#@$) :: TyFun a (a ~> a) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Methods sing :: Sing (<>@#@$) Source #
SOrd a => SingI (InsertSym0 :: TyFun a ([a] ~> [a]) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing InsertSym0 Source #
SEq a => SingI (ElemIndicesSym0 :: TyFun a ([a] ~> [Nat]) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing ElemIndicesSym0 Source #
SEq a => SingI (ElemIndexSym0 :: TyFun a ([a] ~> Maybe Nat) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing ElemIndexSym0 Source #
SEq a => SingI (DeleteSym0 :: TyFun a ([a] ~> [a]) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing DeleteSym0 Source #
SingI (IntersperseSym0 :: TyFun a ([a] ~> [a]) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing IntersperseSym0 Source #
SShow a => SingI (ShowsSym0 :: TyFun a (Symbol ~> Symbol) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Show Methods sing :: Sing ShowsSym0 Source #
SShow a => SingI (Show_Sym0 :: TyFun a Symbol -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Show Methods sing :: Sing Show_Sym0 Source #
SMonoid a => SingI (MappendSym0 :: TyFun a (a ~> a) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Monoid Methods sing :: Sing MappendSym0 Source #
SFoldable t => SingI (OrSym0 :: TyFun (t Bool) Bool -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing OrSym0 Source #
SFoldable t => SingI (AndSym0 :: TyFun (t Bool) Bool -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing AndSym0 Source #
SingI (IntersperseSym0 :: TyFun a (NonEmpty a ~> NonEmpty a) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods sing :: Sing IntersperseSym0 Source #
SOrd a => SingI (InsertSym0 :: TyFun a ([a] ~> NonEmpty a) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods sing :: Sing InsertSym0 Source #
SingI (ConsSym0 :: TyFun a (NonEmpty a ~> NonEmpty a) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods sing :: Sing ConsSym0 Source #
SingI ((<\|@#@$) :: TyFun a (NonEmpty a ~> NonEmpty a) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods sing :: Sing (<\|@#@$) Source #
SingI (AbsurdSym0 :: TyFun Void a -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Void Methods sing :: Sing AbsurdSym0 Source #
SSemigroup a => SingI (SconcatSym0 :: TyFun (NonEmpty a) a -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Methods sing :: Sing SconcatSym0 Source #
SEq a => SingI (NubSym0 :: TyFun (NonEmpty a) (NonEmpty a) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods sing :: Sing NubSym0 Source #
SingI ((!!@#@$) :: TyFun (NonEmpty a) (Nat ~> a) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods sing :: Sing (!!@#@$) Source #
SEq a => SingI (Group1Sym0 :: TyFun (NonEmpty a) (NonEmpty (NonEmpty a)) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods sing :: Sing Group1Sym0 Source #
SingI (ReverseSym0 :: TyFun (NonEmpty a) (NonEmpty a) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods sing :: Sing ReverseSym0 Source #
SingI (ToListSym0 :: TyFun (NonEmpty a) [a] -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods sing :: Sing ToListSym0 Source #
SOrd a => SingI (SortSym0 :: TyFun (NonEmpty a) (NonEmpty a) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods sing :: Sing SortSym0 Source #
SingI (InitSym0 :: TyFun (NonEmpty a) [a] -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods sing :: Sing InitSym0 Source #
SingI (LastSym0 :: TyFun (NonEmpty a) a -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods sing :: Sing LastSym0 Source #
SingI (TailSym0 :: TyFun (NonEmpty a) [a] -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods sing :: Sing TailSym0 Source #
SingI (HeadSym0 :: TyFun (NonEmpty a) a -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods sing :: Sing HeadSym0 Source #
SingI (UnconsSym0 :: TyFun (NonEmpty a) (a, Maybe (NonEmpty a)) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods sing :: Sing UnconsSym0 Source #
SingI (LengthSym0 :: TyFun (NonEmpty a) Nat -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods sing :: Sing LengthSym0 Source #
SingI (TransposeSym0 :: TyFun (NonEmpty (NonEmpty a)) (NonEmpty (NonEmpty a)) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods sing :: Sing TransposeSym0 Source #
SingI d => SingI (ShowParenSym1 d :: TyFun (Symbol ~> Symbol) (Symbol ~> Symbol) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Show Methods sing :: Sing (ShowParenSym1 d) Source #
SingI (UntilSym0 :: TyFun (a ~> Bool) ((a ~> a) ~> (a ~> a)) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Base Methods sing :: Sing UntilSym0 Source #
SingI (UnionBySym0 :: TyFun (a ~> (a ~> Bool)) ([a] ~> ([a] ~> [a])) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing UnionBySym0 Source #
SingI (NubBySym0 :: TyFun (a ~> (a ~> Bool)) ([a] ~> [a]) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing NubBySym0 Source #
SingI (PartitionSym0 :: TyFun (a ~> Bool) ([a] ~> ([a], [a])) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing PartitionSym0 Source #
SingI (GroupBySym0 :: TyFun (a ~> (a ~> Bool)) ([a] ~> [[a]]) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing GroupBySym0 Source #
SingI (BreakSym0 :: TyFun (a ~> Bool) ([a] ~> ([a], [a])) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing BreakSym0 Source #
SingI (SpanSym0 :: TyFun (a ~> Bool) ([a] ~> ([a], [a])) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing SpanSym0 Source #
SingI (DropWhileEndSym0 :: TyFun (a ~> Bool) ([a] ~> [a]) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing DropWhileEndSym0 Source #
SingI (DropWhileSym0 :: TyFun (a ~> Bool) ([a] ~> [a]) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing DropWhileSym0 Source #
SingI (TakeWhileSym0 :: TyFun (a ~> Bool) ([a] ~> [a]) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing TakeWhileSym0 Source #
SingI (IntersectBySym0 :: TyFun (a ~> (a ~> Bool)) ([a] ~> ([a] ~> [a])) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing IntersectBySym0 Source #
SingI (FindIndicesSym0 :: TyFun (a ~> Bool) ([a] ~> [Nat]) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing FindIndicesSym0 Source #
SingI (FindIndexSym0 :: TyFun (a ~> Bool) ([a] ~> Maybe Nat) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing FindIndexSym0 Source #
SingI (FilterSym0 :: TyFun (a ~> Bool) ([a] ~> [a]) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing FilterSym0 Source #
SingI (InsertBySym0 :: TyFun (a ~> (a ~> Ordering)) (a ~> ([a] ~> [a])) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing InsertBySym0 Source #
SingI (SortBySym0 :: TyFun (a ~> (a ~> Ordering)) ([a] ~> [a]) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing SortBySym0 Source #
SingI (DeleteFirstsBySym0 :: TyFun (a ~> (a ~> Bool)) ([a] ~> ([a] ~> [a])) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing DeleteFirstsBySym0 Source #
SingI (DeleteBySym0 :: TyFun (a ~> (a ~> Bool)) (a ~> ([a] ~> [a])) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing DeleteBySym0 Source #
SingI (Scanr1Sym0 :: TyFun (a ~> (a ~> a)) ([a] ~> [a]) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing Scanr1Sym0 Source #
SingI (Scanl1Sym0 :: TyFun (a ~> (a ~> a)) ([a] ~> [a]) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing Scanl1Sym0 Source #
SingI (Foldl1'Sym0 :: TyFun (a ~> (a ~> a)) ([a] ~> a) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing Foldl1'Sym0 Source #
SingI (ShowListWithSym0 :: TyFun (a ~> (Symbol ~> Symbol)) ([a] ~> (Symbol ~> Symbol)) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Show Methods sing :: Sing ShowListWithSym0 Source #
SingI (SortBySym0 :: TyFun (a ~> (a ~> Ordering)) (NonEmpty a ~> NonEmpty a) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods sing :: Sing SortBySym0 Source #
SingI (NubBySym0 :: TyFun (a ~> (a ~> Bool)) (NonEmpty a ~> NonEmpty a) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods sing :: Sing NubBySym0 Source #
SingI (GroupBy1Sym0 :: TyFun (a ~> (a ~> Bool)) (NonEmpty a ~> NonEmpty (NonEmpty a)) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods sing :: Sing GroupBy1Sym0 Source #
SingI (GroupBySym0 :: TyFun (a ~> (a ~> Bool)) ([a] ~> [NonEmpty a]) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods sing :: Sing GroupBySym0 Source #
SingI (PartitionSym0 :: TyFun (a ~> Bool) (NonEmpty a ~> ([a], [a])) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods sing :: Sing PartitionSym0 Source #
SingI (FilterSym0 :: TyFun (a ~> Bool) (NonEmpty a ~> [a]) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods sing :: Sing FilterSym0 Source #
SingI (BreakSym0 :: TyFun (a ~> Bool) (NonEmpty a ~> ([a], [a])) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods sing :: Sing BreakSym0 Source #
SingI (SpanSym0 :: TyFun (a ~> Bool) (NonEmpty a ~> ([a], [a])) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods sing :: Sing SpanSym0 Source #
SingI (DropWhileSym0 :: TyFun (a ~> Bool) (NonEmpty a ~> [a]) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods sing :: Sing DropWhileSym0 Source #
SingI (TakeWhileSym0 :: TyFun (a ~> Bool) (NonEmpty a ~> [a]) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods sing :: Sing TakeWhileSym0 Source #
SingI (Scanr1Sym0 :: TyFun (a ~> (a ~> a)) (NonEmpty a ~> NonEmpty a) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods sing :: Sing Scanr1Sym0 Source #
SingI (Scanl1Sym0 :: TyFun (a ~> (a ~> a)) (NonEmpty a ~> NonEmpty a) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods sing :: Sing Scanl1Sym0 Source #
SingI ((:$$:@#@$) :: TyFun (ErrorMessage' Symbol) (ErrorMessage' Symbol ~> ErrorMessage' Symbol) -> Type) Source #
Instance details Defined in Data.Singletons.TypeError Methods sing :: Sing (:$$:@#@$) Source #
SingI ((:<>:@#@$) :: TyFun (ErrorMessage' Symbol) (ErrorMessage' Symbol ~> ErrorMessage' Symbol) -> Type) Source #
Instance details Defined in Data.Singletons.TypeError Methods sing :: Sing (:<>:@#@$) Source #
SingI (Tuple2Sym0 :: TyFun a (b ~> (a, b)) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing Tuple2Sym0 Source #
SingI d => SingI ((:@#@$$) d :: TyFun [a] [a] -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing ((:@#@$$) d) Source #
SingI d => SingI (IntercalateSym1 d :: TyFun [[a]] [a] -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (IntercalateSym1 d) Source #
SingI (RightsSym0 :: TyFun [Either a b] [b] -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Either Methods sing :: Sing RightsSym0 Source #
SingI (LeftsSym0 :: TyFun [Either a b] [a] -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Either Methods sing :: Sing LeftsSym0 Source #
SingI (UnzipSym0 :: TyFun [(a, b)] ([a], [b]) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing UnzipSym0 Source #
SingI d => SingI ((:\|@#@$$) d :: TyFun [a] (NonEmpty a) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing ((:\|@#@$$) d) Source #
SingI d => SingI ((++@#@$$) d :: TyFun [a] [a] -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Base Methods sing :: Sing ((++@#@$$) d) Source #
SNum i => SingI (GenericLengthSym0 :: TyFun [a] i -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing GenericLengthSym0 Source #
(SEq a, SingI d) => SingI (UnionSym1 d :: TyFun [a] [a] -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (UnionSym1 d) Source #
SingI d => SingI (UnionBySym1 d :: TyFun [a] ([a] ~> [a]) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (UnionBySym1 d) Source #
SingI d => SingI (NubBySym1 d :: TyFun [a] [a] -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (NubBySym1 d) Source #
SingI d => SingI (PartitionSym1 d :: TyFun [a] ([a], [a]) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (PartitionSym1 d) Source #
SingI d => SingI (GroupBySym1 d :: TyFun [a] [[a]] -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (GroupBySym1 d) Source #
(SOrd a, SingI d) => SingI (InsertSym1 d :: TyFun [a] [a] -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (InsertSym1 d) Source #
SingI d => SingI (SplitAtSym1 d a :: TyFun [a] ([a], [a]) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (SplitAtSym1 d a) Source #
SingI d => SingI (DropSym1 d a :: TyFun [a] [a] -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (DropSym1 d a) Source #
SingI d => SingI (TakeSym1 d a :: TyFun [a] [a] -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (TakeSym1 d a) Source #
SingI d => SingI (BreakSym1 d :: TyFun [a] ([a], [a]) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (BreakSym1 d) Source #
SingI d => SingI (SpanSym1 d :: TyFun [a] ([a], [a]) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (SpanSym1 d) Source #
SingI d => SingI (DropWhileEndSym1 d :: TyFun [a] [a] -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (DropWhileEndSym1 d) Source #
SingI d => SingI (DropWhileSym1 d :: TyFun [a] [a] -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (DropWhileSym1 d) Source #
SingI d => SingI (TakeWhileSym1 d :: TyFun [a] [a] -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (TakeWhileSym1 d) Source #
SingI d => SingI (IntersectBySym1 d :: TyFun [a] ([a] ~> [a]) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (IntersectBySym1 d) Source #
(SEq a, SingI d) => SingI (IntersectSym1 d :: TyFun [a] [a] -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (IntersectSym1 d) Source #
SingI d => SingI (FindIndicesSym1 d :: TyFun [a] [Nat] -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (FindIndicesSym1 d) Source #
SingI d => SingI (FindIndexSym1 d :: TyFun [a] (Maybe Nat) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (FindIndexSym1 d) Source #
(SEq a, SingI d) => SingI (ElemIndicesSym1 d :: TyFun [a] [Nat] -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (ElemIndicesSym1 d) Source #
(SEq a, SingI d) => SingI (ElemIndexSym1 d :: TyFun [a] (Maybe Nat) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (ElemIndexSym1 d) Source #
SingI d => SingI (FilterSym1 d :: TyFun [a] [a] -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (FilterSym1 d) Source #
SingI d => SingI (SortBySym1 d :: TyFun [a] [a] -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (SortBySym1 d) Source #
SingI d => SingI (DeleteFirstsBySym1 d :: TyFun [a] ([a] ~> [a]) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (DeleteFirstsBySym1 d) Source #
(SEq a, SingI d) => SingI ((\\@#@$$) d :: TyFun [a] [a] -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing ((\\@#@$$) d) Source #
(SEq a, SingI d) => SingI (DeleteSym1 d :: TyFun [a] [a] -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (DeleteSym1 d) Source #
SingI (ZipSym0 :: TyFun [a] ([b] ~> [(a, b)]) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing ZipSym0 Source #
(SEq a, SingI d) => SingI (IsInfixOfSym1 d :: TyFun [a] Bool -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (IsInfixOfSym1 d) Source #
(SEq a, SingI d) => SingI (IsSuffixOfSym1 d :: TyFun [a] Bool -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (IsSuffixOfSym1 d) Source #
(SEq a, SingI d) => SingI (IsPrefixOfSym1 d :: TyFun [a] Bool -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (IsPrefixOfSym1 d) Source #
SingI d => SingI (Scanr1Sym1 d :: TyFun [a] [a] -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (Scanr1Sym1 d) Source #
SingI d => SingI (Scanl1Sym1 d :: TyFun [a] [a] -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (Scanl1Sym1 d) Source #
SingI d => SingI (Foldl1'Sym1 d :: TyFun [a] a -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (Foldl1'Sym1 d) Source #
SingI d => SingI (IntersperseSym1 d :: TyFun [a] [a] -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (IntersperseSym1 d) Source #
SingI d => SingI (ShowListWithSym1 d :: TyFun [a] (Symbol ~> Symbol) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Show Methods sing :: Sing (ShowListWithSym1 d) Source #
SingI d => SingI (GroupBySym1 d :: TyFun [a] [NonEmpty a] -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods sing :: Sing (GroupBySym1 d) Source #
(SOrd a, SingI d) => SingI (InsertSym1 d :: TyFun [a] (NonEmpty a) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods sing :: Sing (InsertSym1 d) Source #
SingI d => SingI (FromMaybeSym1 d :: TyFun (Maybe a) a -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Maybe Methods sing :: Sing (FromMaybeSym1 d) Source #
SingI (IsRightSym0 :: TyFun (Either a b) Bool -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Either Methods sing :: Sing IsRightSym0 Source #
SingI (IsLeftSym0 :: TyFun (Either a b) Bool -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Either Methods sing :: Sing IsLeftSym0 Source #
SingI d => SingI ((!!@#@$$) d :: TyFun Nat a -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing ((!!@#@$$) d) Source #
SingI d => SingI ((!!@#@$$) d :: TyFun Nat a -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods sing :: Sing ((!!@#@$$) d) Source #
SApplicative m => SingI (ReplicateM_Sym0 :: TyFun Nat (m a ~> m ()) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Monad Methods sing :: Sing ReplicateM_Sym0 Source #
SApplicative m => SingI (ReplicateMSym0 :: TyFun Nat (m a ~> m [a]) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Monad Methods sing :: Sing ReplicateMSym0 Source #
(SShow a, SingI d) => SingI (ShowListSym1 d :: TyFun Symbol Symbol -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Show Methods sing :: Sing (ShowListSym1 d) Source #
(SShow a, SingI d) => SingI (ShowsSym1 d :: TyFun Symbol Symbol -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Show Methods sing :: Sing (ShowsSym1 d) Source #
(SingI d1, SingI d2) => SingI (ShowParenSym2 d1 d2 :: TyFun Symbol Symbol -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Show Methods sing :: Sing (ShowParenSym2 d1 d2) Source #
SingI (ErrorSym0 :: TyFun Symbol a -> Type) Source #
Instance details Defined in Data.Singletons.TypeLits.Internal Methods sing :: Sing ErrorSym0 Source #
SingI (ErrorWithoutStackTraceSym0 :: TyFun Symbol a -> Type) Source #
Instance details Defined in Data.Singletons.TypeLits.Internal Methods sing :: Sing ErrorWithoutStackTraceSym0 Source #
SingI (SwapSym0 :: TyFun (a, b) (b, a) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Tuple Methods sing :: Sing SwapSym0 Source #
SingI (SndSym0 :: TyFun (a, b) b -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Tuple Methods sing :: Sing SndSym0 Source #
SingI (FstSym0 :: TyFun (a, b) a -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Tuple Methods sing :: Sing FstSym0 Source #
SingI (ArgSym0 :: TyFun a (b ~> Arg a b) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods sing :: Sing ArgSym0 Source #
SingI (LeftSym0 :: TyFun a (Either a b) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing LeftSym0 Source #
SingI (RightSym0 :: TyFun b (Either a b) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing RightSym0 Source #
SingI d => SingI (Bool_Sym1 d :: TyFun a (Bool ~> a) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Bool Methods sing :: Sing (Bool_Sym1 d) Source #
(SEq a, SingI x) => SingI ((/=@#@$$) x :: TyFun a Bool -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Eq Methods sing :: Sing ((/=@#@$$) x) Source #
(SEq a, SingI x) => SingI ((==@#@$$) x :: TyFun a Bool -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Eq Methods sing :: Sing ((==@#@$$) x) Source #
(SOrd a, SingI d) => SingI ((>=@#@$$) d :: TyFun a Bool -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Ord Methods sing :: Sing ((>=@#@$$) d) Source #
(SOrd a, SingI d) => SingI ((>@#@$$) d :: TyFun a Bool -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Ord Methods sing :: Sing ((>@#@$$) d) Source #
(SOrd a, SingI d) => SingI ((<=@#@$$) d :: TyFun a Bool -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Ord Methods sing :: Sing ((<=@#@$$) d) Source #
(SOrd a, SingI d) => SingI ((<@#@$$) d :: TyFun a Bool -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Ord Methods sing :: Sing ((<@#@$$) d) Source #
(SOrd a, SingI d) => SingI (CompareSym1 d :: TyFun a Ordering -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Ord Methods sing :: Sing (CompareSym1 d) Source #
(SOrd a, SingI d) => SingI (MinSym1 d :: TyFun a a -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Ord Methods sing :: Sing (MinSym1 d) Source #
(SOrd a, SingI d) => SingI (MaxSym1 d :: TyFun a a -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Ord Methods sing :: Sing (MaxSym1 d) Source #
SingI (Maybe_Sym0 :: TyFun b ((a ~> b) ~> (Maybe a ~> b)) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Maybe Methods sing :: Sing Maybe_Sym0 Source #
(SNum a, SingI d) => SingI ((*@#@$$) d :: TyFun a a -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Num Methods sing :: Sing ((*@#@$$) d) Source #
(SNum a, SingI d) => SingI ((-@#@$$) d :: TyFun a a -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Num Methods sing :: Sing ((-@#@$$) d) Source #
(SNum a, SingI d) => SingI ((+@#@$$) d :: TyFun a a -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Num Methods sing :: Sing ((+@#@$$) d) Source #
(SNum a, SingI d) => SingI (SubtractSym1 d :: TyFun a a -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Num Methods sing :: Sing (SubtractSym1 d) Source #
SingI (SeqSym0 :: TyFun a (b ~> b) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Base Methods sing :: Sing SeqSym0 Source #
SingI d => SingI (AsTypeOfSym1 d :: TyFun a a -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Base Methods sing :: Sing (AsTypeOfSym1 d) Source #
SingI (ConstSym0 :: TyFun a (b ~> a) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Base Methods sing :: Sing ConstSym0 Source #
(SApplicative f, SingI d) => SingI (WhenSym1 d f :: TyFun (f ()) (f ()) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing (WhenSym1 d f) Source #
SMonad m => SingI (JoinSym0 :: TyFun (m (m a)) (m a) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing JoinSym0 Source #
SApplicative f => SingI (PureSym0 :: TyFun a (f a) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing PureSym0 Source #
SMonad m => SingI (ReturnSym0 :: TyFun a (m a) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing ReturnSym0 Source #
SFunctor f => SingI (VoidSym0 :: TyFun (f a) (f ()) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Functor Methods sing :: Sing VoidSym0 Source #
SingI ((&@#@$) :: TyFun a ((a ~> b) ~> b) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Function Methods sing :: Sing (&@#@$) Source #
(SEnum a, SingI d) => SingI (EnumFromToSym1 d :: TyFun a [a] -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Enum Methods sing :: Sing (EnumFromToSym1 d) Source #
(SEnum a, SingI d) => SingI (EnumFromThenToSym1 d :: TyFun a (a ~> [a]) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Enum Methods sing :: Sing (EnumFromThenToSym1 d) Source #
(SSemigroup a, SingI d) => SingI ((<>@#@$$) d :: TyFun a a -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Methods sing :: Sing ((<>@#@$$) d) Source #
SingI d => SingI (ReplicateSym1 d a :: TyFun a [a] -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (ReplicateSym1 d a) Source #
SEq a => SingI (LookupSym0 :: TyFun a ([(a, b)] ~> Maybe b) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing LookupSym0 Source #
SingI d => SingI (InsertBySym1 d :: TyFun a ([a] ~> [a]) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (InsertBySym1 d) Source #
SingI d => SingI (DeleteBySym1 d :: TyFun a ([a] ~> [a]) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (DeleteBySym1 d) Source #
(SShow a, SingI d) => SingI (ShowsPrecSym1 d a :: TyFun a (Symbol ~> Symbol) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Show Methods sing :: Sing (ShowsPrecSym1 d a) Source #
(SMonoid a, SingI d) => SingI (MappendSym1 d :: TyFun a a -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Monoid Methods sing :: Sing (MappendSym1 d) Source #
(SFoldable t, SEq a) => SingI (NotElemSym0 :: TyFun a (t a ~> Bool) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing NotElemSym0 Source #
SFoldable t => SingI (ConcatSym0 :: TyFun (t [a]) [a] -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing ConcatSym0 Source #
(SFoldable t, SMonoid m) => SingI (FoldSym0 :: TyFun (t m) m -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing FoldSym0 Source #
SFoldable t => SingI (ToListSym0 :: TyFun (t a) [a] -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing ToListSym0 Source #
(SFoldable t, SOrd a) => SingI (MaximumSym0 :: TyFun (t a) a -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing MaximumSym0 Source #
(SFoldable t, SOrd a) => SingI (MinimumSym0 :: TyFun (t a) a -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing MinimumSym0 Source #
(SFoldable t, SNum a) => SingI (SumSym0 :: TyFun (t a) a -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing SumSym0 Source #
(SFoldable t, SNum a) => SingI (ProductSym0 :: TyFun (t a) a -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing ProductSym0 Source #
(SFoldable t, SEq a) => SingI (ElemSym0 :: TyFun a (t a ~> Bool) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing ElemSym0 Source #
SAlternative f => SingI (OptionalSym0 :: TyFun (f a) (f (Maybe a)) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Applicative Methods sing :: Sing OptionalSym0 Source #
(SApplicative f, SingI d) => SingI (UnlessSym1 d f :: TyFun (f ()) (f ()) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Monad Methods sing :: Sing (UnlessSym1 d f) Source #
SingI (ShowTypeSym0 :: TyFun t (ErrorMessage' Symbol) -> Type) Source #
Instance details Defined in Data.Singletons.TypeError Methods sing :: Sing ShowTypeSym0 Source #
SingI (UnzipSym0 :: TyFun (NonEmpty (a, b)) (NonEmpty a, NonEmpty b) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods sing :: Sing UnzipSym0 Source #
SingI d => SingI (SortBySym1 d :: TyFun (NonEmpty a) (NonEmpty a) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods sing :: Sing (SortBySym1 d) Source #
SingI d => SingI (NubBySym1 d :: TyFun (NonEmpty a) (NonEmpty a) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods sing :: Sing (NubBySym1 d) Source #
SingI (ZipSym0 :: TyFun (NonEmpty a) (NonEmpty b ~> NonEmpty (a, b)) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods sing :: Sing ZipSym0 Source #
(SEq a, SingI d) => SingI (IsPrefixOfSym1 d :: TyFun (NonEmpty a) Bool -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods sing :: Sing (IsPrefixOfSym1 d) Source #
SingI d => SingI (GroupBy1Sym1 d :: TyFun (NonEmpty a) (NonEmpty (NonEmpty a)) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods sing :: Sing (GroupBy1Sym1 d) Source #
SingI d => SingI (PartitionSym1 d :: TyFun (NonEmpty a) ([a], [a]) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods sing :: Sing (PartitionSym1 d) Source #
SingI d => SingI (FilterSym1 d :: TyFun (NonEmpty a) [a] -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods sing :: Sing (FilterSym1 d) Source #
SingI d => SingI (BreakSym1 d :: TyFun (NonEmpty a) ([a], [a]) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods sing :: Sing (BreakSym1 d) Source #
SingI d => SingI (SpanSym1 d :: TyFun (NonEmpty a) ([a], [a]) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods sing :: Sing (SpanSym1 d) Source #
SingI d => SingI (DropWhileSym1 d :: TyFun (NonEmpty a) [a] -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods sing :: Sing (DropWhileSym1 d) Source #
SingI d => SingI (TakeWhileSym1 d :: TyFun (NonEmpty a) [a] -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods sing :: Sing (TakeWhileSym1 d) Source #
SingI d => SingI (SplitAtSym1 d a :: TyFun (NonEmpty a) ([a], [a]) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods sing :: Sing (SplitAtSym1 d a) Source #
SingI d => SingI (DropSym1 d a :: TyFun (NonEmpty a) [a] -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods sing :: Sing (DropSym1 d a) Source #
SingI d => SingI (TakeSym1 d a :: TyFun (NonEmpty a) [a] -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods sing :: Sing (TakeSym1 d a) Source #
SingI d => SingI (IntersperseSym1 d :: TyFun (NonEmpty a) (NonEmpty a) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods sing :: Sing (IntersperseSym1 d) Source #
SingI d => SingI (Scanr1Sym1 d :: TyFun (NonEmpty a) (NonEmpty a) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods sing :: Sing (Scanr1Sym1 d) Source #
SingI d => SingI (Scanl1Sym1 d :: TyFun (NonEmpty a) (NonEmpty a) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods sing :: Sing (Scanl1Sym1 d) Source #
SingI d => SingI (ConsSym1 d :: TyFun (NonEmpty a) (NonEmpty a) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods sing :: Sing (ConsSym1 d) Source #
SingI d => SingI ((<\|@#@$$) d :: TyFun (NonEmpty a) (NonEmpty a) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods sing :: Sing ((<\|@#@$$) d) Source #
SOrd a => SingI (ComparingSym0 :: TyFun (b ~> a) (b ~> (b ~> Ordering)) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Ord Methods sing :: Sing ComparingSym0 Source #
SingI (MapMaybeSym0 :: TyFun (a ~> Maybe b) ([a] ~> [b]) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Maybe Methods sing :: Sing MapMaybeSym0 Source #
SingI d => SingI (UntilSym1 d :: TyFun (a ~> a) (a ~> a) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Base Methods sing :: Sing (UntilSym1 d) Source #
SingI (($!@#@$) :: TyFun (a ~> b) (a ~> b) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Base Methods sing :: Sing ($!@#@$) Source #
SingI (($@#@$) :: TyFun (a ~> b) (a ~> b) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Base Methods sing :: Sing ($@#@$) Source #
SingI (MapSym0 :: TyFun (a ~> b) ([a] ~> [b]) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Base Methods sing :: Sing MapSym0 Source #
SingI (FoldrSym0 :: TyFun (a ~> (b ~> b)) (b ~> ([a] ~> b)) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Base Methods sing :: Sing FoldrSym0 Source #
SingI (UnfoldrSym0 :: TyFun (b ~> Maybe (a, b)) (b ~> [a]) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing UnfoldrSym0 Source #
SingI (ScanrSym0 :: TyFun (a ~> (b ~> b)) (b ~> ([a] ~> [b])) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing ScanrSym0 Source #
SingI (ScanlSym0 :: TyFun (b ~> (a ~> b)) (b ~> ([a] ~> [b])) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing ScanlSym0 Source #
SFoldable t => SingI (FindSym0 :: TyFun (a ~> Bool) (t a ~> Maybe a) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing FindSym0 Source #
SFoldable t => SingI (MinimumBySym0 :: TyFun (a ~> (a ~> Ordering)) (t a ~> a) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing MinimumBySym0 Source #
SFoldable t => SingI (MaximumBySym0 :: TyFun (a ~> (a ~> Ordering)) (t a ~> a) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing MaximumBySym0 Source #
SFoldable t => SingI (AllSym0 :: TyFun (a ~> Bool) (t a ~> Bool) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing AllSym0 Source #
SFoldable t => SingI (AnySym0 :: TyFun (a ~> Bool) (t a ~> Bool) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing AnySym0 Source #
SFoldable t => SingI (Foldr1Sym0 :: TyFun (a ~> (a ~> a)) (t a ~> a) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing Foldr1Sym0 Source #
SFoldable t => SingI (Foldl1Sym0 :: TyFun (a ~> (a ~> a)) (t a ~> a) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing Foldl1Sym0 Source #
SOrd o => SingI (SortWithSym0 :: TyFun (a ~> o) (NonEmpty a ~> NonEmpty a) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods sing :: Sing SortWithSym0 Source #
SOrd b => SingI (GroupAllWith1Sym0 :: TyFun (a ~> b) (NonEmpty a ~> NonEmpty (NonEmpty a)) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods sing :: Sing GroupAllWith1Sym0 Source #
SEq b => SingI (GroupWith1Sym0 :: TyFun (a ~> b) (NonEmpty a ~> NonEmpty (NonEmpty a)) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods sing :: Sing GroupWith1Sym0 Source #
SOrd b => SingI (GroupAllWithSym0 :: TyFun (a ~> b) ([a] ~> [NonEmpty a]) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods sing :: Sing GroupAllWithSym0 Source #
SEq b => SingI (GroupWithSym0 :: TyFun (a ~> b) ([a] ~> [NonEmpty a]) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods sing :: Sing GroupWithSym0 Source #
SingI (ScanrSym0 :: TyFun (a ~> (b ~> b)) (b ~> ([a] ~> NonEmpty b)) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods sing :: Sing ScanrSym0 Source #
SingI (ScanlSym0 :: TyFun (b ~> (a ~> b)) (b ~> ([a] ~> NonEmpty b)) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods sing :: Sing ScanlSym0 Source #
SingI (MapSym0 :: TyFun (a ~> b) (NonEmpty a ~> NonEmpty b) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods sing :: Sing MapSym0 Source #
SingI (UnfoldrSym0 :: TyFun (a ~> (b, Maybe a)) (a ~> NonEmpty b) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods sing :: Sing UnfoldrSym0 Source #
SingI (UnfoldSym0 :: TyFun (a ~> (b, Maybe a)) (a ~> NonEmpty b) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods sing :: Sing UnfoldSym0 Source #
SMonadPlus m => SingI (MfilterSym0 :: TyFun (a ~> Bool) (m a ~> m a) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Monad Methods sing :: Sing MfilterSym0 Source #
SApplicative m => SingI (FilterMSym0 :: TyFun (a ~> m Bool) ([a] ~> m [a]) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Monad Methods sing :: Sing FilterMSym0 Source #
SingI x => SingI ((:$$:@#@$$) x :: TyFun (ErrorMessage' Symbol) (ErrorMessage' Symbol) -> Type) Source #
Instance details Defined in Data.Singletons.TypeError Methods sing :: Sing ((:$$:@#@$$) x) Source #
SingI x => SingI ((:<>:@#@$$) x :: TyFun (ErrorMessage' Symbol) (ErrorMessage' Symbol) -> Type) Source #
Instance details Defined in Data.Singletons.TypeError Methods sing :: Sing ((:<>:@#@$$) x) Source #
SingI (TyCon1 (Const :: k1 -> Const k1 b) :: k1 ~> Const k1 b) Source #
Instance details Defined in Data.Singletons.Prelude.Const Methods sing :: Sing (TyCon1 Const0) Source #
SingI (ConstSym0 :: TyFun a6989586621679086334 (Const a6989586621679086334 b6989586621679086335) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Const Methods sing :: Sing ConstSym0 Source #
SingI n => SingI (Left n :: Either a b) Source #
Instance details Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing (Left n) Source #
SingI n => SingI (Right n :: Either a b) Source #
Instance details Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing (Right n) Source #
SingI (TyCon1 (Just :: a -> Maybe a) :: a ~> Maybe a) Source #
Instance details Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing (TyCon1 Just) Source #
SingI (Tuple3Sym0 :: TyFun a (b ~> (c ~> (a, b, c))) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing Tuple3Sym0 Source #
SingI d => SingI (TyCon1 ((,) d :: b -> (a, b)) :: b ~> (a, b)) Source #
Instance details Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing (TyCon1 ((,) d)) Source #
SingI d => SingI (Tuple2Sym1 d b :: TyFun b (a, b) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing (Tuple2Sym1 d b) Source #
(SingI d1, SingI d2) => SingI (TyCon1 ((,,) d1 d2 :: c -> (a, b, c)) :: c ~> (a, b, c)) Source #
Instance details Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing (TyCon1 ((,,) d1 d2)) Source #
(SingI d2, SingI d3, SingI d4) => SingI (TyCon1 ((,,,) d2 d3 d4 :: d1 -> (a, b, c, d1)) :: d1 ~> (a, b, c, d1)) Source #
Instance details Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing (TyCon1 ((,,,) d2 d3 d4)) Source #
(SingI d2, SingI d3, SingI d4, SingI d5) => SingI (TyCon1 ((,,,,) d2 d3 d4 d5 :: e -> (a, b, c, d1, e)) :: e ~> (a, b, c, d1, e)) Source #
Instance details Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing (TyCon1 ((,,,,) d2 d3 d4 d5)) Source #
(SingI d2, SingI d3, SingI d4, SingI d5, SingI d6) => SingI (TyCon1 ((,,,,,) d2 d3 d4 d5 d6 :: f -> (a, b, c, d1, e, f)) :: f ~> (a, b, c, d1, e, f)) Source #
Instance details Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing (TyCon1 ((,,,,,) d2 d3 d4 d5 d6)) Source #
(SingI d2, SingI d3, SingI d4, SingI d5, SingI d6, SingI d7) => SingI (TyCon1 ((,,,,,,) d2 d3 d4 d5 d6 d7 :: g -> (a, b, c, d1, e, f, g)) :: g ~> (a, b, c, d1, e, f, g)) Source #
Instance details Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing (TyCon1 ((,,,,,,) d2 d3 d4 d5 d6 d7)) Source #
(SingI d1, SingI d2) => SingI (Bool_Sym2 d1 d2 :: TyFun Bool a -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Bool Methods sing :: Sing (Bool_Sym2 d1 d2) Source #
SingI (TyCon1 All) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Methods sing :: Sing (TyCon1 All) Source #
SingI (TyCon1 Any) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Methods sing :: Sing (TyCon1 Any) Source #
SingI d => SingI (TyCon1 ((:) d) :: [a] ~> [a]) Source #
Instance details Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing (TyCon1 ((:) d)) Source #
(SEq a, SingI d) => SingI (LookupSym1 d b :: TyFun [(a, b)] (Maybe b) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (LookupSym1 d b) Source #
SingI (Unzip3Sym0 :: TyFun [(a, b, c)] ([a], [b], [c]) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing Unzip3Sym0 Source #
SingI d => SingI (TyCon1 ((:\|) d) :: [a] ~> NonEmpty a) Source #
Instance details Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing (TyCon1 ((:\|) d)) Source #
SingI d => SingI (MapMaybeSym1 d :: TyFun [a] [b] -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Maybe Methods sing :: Sing (MapMaybeSym1 d) Source #
SingI d => SingI (MapSym1 d :: TyFun [a] [b] -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Base Methods sing :: Sing (MapSym1 d) Source #
(SingI d1, SingI d2) => SingI (UnionBySym2 d1 d2 :: TyFun [a] [a] -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (UnionBySym2 d1 d2) Source #
(SingI d1, SingI d2) => SingI (IntersectBySym2 d1 d2 :: TyFun [a] [a] -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (IntersectBySym2 d1 d2) Source #
(SingI d1, SingI d2) => SingI (InsertBySym2 d1 d2 :: TyFun [a] [a] -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (InsertBySym2 d1 d2) Source #
(SingI d1, SingI d2) => SingI (DeleteFirstsBySym2 d1 d2 :: TyFun [a] [a] -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (DeleteFirstsBySym2 d1 d2) Source #
(SingI d1, SingI d2) => SingI (DeleteBySym2 d1 d2 :: TyFun [a] [a] -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (DeleteBySym2 d1 d2) Source #
SingI (Zip3Sym0 :: TyFun [a] ([b] ~> ([c] ~> [(a, b, c)])) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing Zip3Sym0 Source #
SingI d => SingI (ZipSym1 d b :: TyFun [b] [(a, b)] -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (ZipSym1 d b) Source #
(SOrd b, SingI d) => SingI (GroupAllWithSym1 d :: TyFun [a] [NonEmpty a] -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods sing :: Sing (GroupAllWithSym1 d) Source #
(SEq b, SingI d) => SingI (GroupWithSym1 d :: TyFun [a] [NonEmpty a] -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods sing :: Sing (GroupWithSym1 d) Source #
(SApplicative m, SingI d) => SingI (FilterMSym1 d :: TyFun [a] (m [a]) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Monad Methods sing :: Sing (FilterMSym1 d) Source #
SingI (TyCon1 (Option :: Maybe a -> Option a) :: Maybe a ~> Option a) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Methods sing :: Sing (TyCon1 Option0) Source #
SingI (TyCon1 (Last :: Maybe a -> Last a) :: Maybe a ~> Last a) Source #
Instance details Defined in Data.Singletons.Prelude.Monoid Methods sing :: Sing (TyCon1 Last0) Source #
SingI (TyCon1 (First :: Maybe a -> First a) :: Maybe a ~> First a) Source #
Instance details Defined in Data.Singletons.Prelude.Monoid Methods sing :: Sing (TyCon1 First0) Source #
(SShow a, SingI d1, SingI d2) => SingI (ShowsPrecSym2 d1 d2 :: TyFun Symbol Symbol -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Show Methods sing :: Sing (ShowsPrecSym2 d1 d2) Source #
(SingI d1, SingI d2) => SingI (ShowListWithSym2 d1 d2 :: TyFun Symbol Symbol -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Show Methods sing :: Sing (ShowListWithSym2 d1 d2) Source #
SMonad m => SingI (FailSym0 :: TyFun Symbol (m a) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing FailSym0 Source #
SingI (TyCon1 (Text :: Symbol -> ErrorMessage' Symbol)) Source #
Instance details Defined in Data.Singletons.TypeError Methods sing :: Sing (TyCon1 Text) Source #
SingI (TyCon1 (Min :: a -> Min a) :: a ~> Min a) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Methods sing :: Sing (TyCon1 Min0) Source #
SingI (TyCon1 (Max :: a -> Max a) :: a ~> Max a) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Methods sing :: Sing (TyCon1 Max0) Source #
SingI d => SingI (TyCon1 (Arg d :: b -> Arg a b) :: b ~> Arg a b) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods sing :: Sing (TyCon1 (Arg0 d)) Source #
SingI d => SingI (ArgSym1 d b :: TyFun b (Arg a b) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods sing :: Sing (ArgSym1 d b) Source #
SingI (TyCon1 (First :: a -> First a) :: a ~> First a) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Methods sing :: Sing (TyCon1 First0) Source #
SingI (TyCon1 (Last :: a -> Last a) :: a ~> Last a) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Methods sing :: Sing (TyCon1 Last0) Source #
SingI (TyCon1 (WrapMonoid :: m -> WrappedMonoid m) :: m ~> WrappedMonoid m) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Methods sing :: Sing (TyCon1 WrapMonoid) Source #
SingI (TyCon1 (Sum :: a -> Sum a) :: a ~> Sum a) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Methods sing :: Sing (TyCon1 Sum0) Source #
SingI (TyCon1 (Product :: a -> Product a) :: a ~> Product a) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Methods sing :: Sing (TyCon1 Product0) Source #
SingI (TyCon1 (Dual :: a -> Dual a) :: a ~> Dual a) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Methods sing :: Sing (TyCon1 Dual0) Source #
SingI (TyCon1 (Identity :: a -> Identity a) :: a ~> Identity a) Source #
Instance details Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing (TyCon1 Identity0) Source #
SingI (TyCon1 (Left :: a -> Either a b) :: a ~> Either a b) Source #
Instance details Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing (TyCon1 Left) Source #
SingI (TyCon1 (Right :: b -> Either a b) :: b ~> Either a b) Source #
Instance details Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing (TyCon1 Right) Source #
SingI (TyCon1 (Down :: a -> Down a) :: a ~> Down a) Source #
Instance details Defined in Data.Singletons.Prelude.Ord Methods sing :: Sing (TyCon1 Down0) Source #
(SOrd a, SingI d) => SingI (ComparingSym1 d :: TyFun b (b ~> Ordering) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Ord Methods sing :: Sing (ComparingSym1 d) Source #
SingI d => SingI (SeqSym1 d b :: TyFun b b -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Base Methods sing :: Sing (SeqSym1 d b) Source #
(SingI d1, SingI d2) => SingI (UntilSym2 d1 d2 :: TyFun a a -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Base Methods sing :: Sing (UntilSym2 d1 d2) Source #
SingI d => SingI (($!@#@$$) d :: TyFun a b -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Base Methods sing :: Sing (($!@#@$$) d) Source #
SingI d => SingI (($@#@$$) d :: TyFun a b -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Base Methods sing :: Sing (($@#@$$) d) Source #
SingI d => SingI (ConstSym1 d b :: TyFun b a -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Base Methods sing :: Sing (ConstSym1 d b) Source #
SingI d => SingI (FoldrSym1 d :: TyFun b ([a] ~> b) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Base Methods sing :: Sing (FoldrSym1 d) Source #
SMonad m => SingI (ApSym0 :: TyFun (m (a ~> b)) (m a ~> m b) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing ApSym0 Source #
SApplicative f => SingI ((<**>@#@$) :: TyFun (f a) (f (a ~> b) ~> f b) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing (<**>@#@$) Source #
SFunctor f => SingI ((<$@#@$) :: TyFun a (f b ~> f a) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing (<$@#@$) Source #
SApplicative f => SingI ((<*>@#@$) :: TyFun (f (a ~> b)) (f a ~> f b) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing (<*>@#@$) Source #
SMonad m => SingI ((>>=@#@$) :: TyFun (m a) ((a ~> m b) ~> m b) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing (>>=@#@$) Source #
SAlternative f => SingI ((<\|>@#@$) :: TyFun (f a) (f a ~> f a) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing (<\|>@#@$) Source #
SMonadPlus m => SingI (MplusSym0 :: TyFun (m a) (m a ~> m a) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing MplusSym0 Source #
SFunctor f => SingI (($>@#@$) :: TyFun (f a) (b ~> f b) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Functor Methods sing :: Sing ($>@#@$) Source #
SFunctor f => SingI ((<&>@#@$) :: TyFun (f a) ((a ~> b) ~> f b) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Functor Methods sing :: Sing (<&>@#@$) Source #
(SEnum a, SingI d1, SingI d2) => SingI (EnumFromThenToSym2 d1 d2 :: TyFun a [a] -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Enum Methods sing :: Sing (EnumFromThenToSym2 d1 d2) Source #
SingI d => SingI (UnfoldrSym1 d :: TyFun b [a] -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (UnfoldrSym1 d) Source #
SingI d => SingI (ScanrSym1 d :: TyFun b ([a] ~> [b]) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (ScanrSym1 d) Source #
SingI d => SingI (ScanlSym1 d :: TyFun b ([a] ~> [b]) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (ScanlSym1 d) Source #
(SFoldable t, SingI d) => SingI (FindSym1 d t :: TyFun (t a) (Maybe a) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing (FindSym1 d t) Source #
(SFoldable t, SEq a, SingI d) => SingI (NotElemSym1 d t :: TyFun (t a) Bool -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing (NotElemSym1 d t) Source #
(SFoldable t, SingI d) => SingI (MinimumBySym1 d t :: TyFun (t a) a -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing (MinimumBySym1 d t) Source #
(SFoldable t, SingI d) => SingI (MaximumBySym1 d t :: TyFun (t a) a -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing (MaximumBySym1 d t) Source #
(SFoldable t, SingI d) => SingI (AllSym1 d t :: TyFun (t a) Bool -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing (AllSym1 d t) Source #
(SFoldable t, SingI d) => SingI (AnySym1 d t :: TyFun (t a) Bool -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing (AnySym1 d t) Source #
(SFoldable t, SMonad m) => SingI (Sequence_Sym0 :: TyFun (t (m a)) (m ()) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing Sequence_Sym0 Source #
(SFoldable t, SApplicative f) => SingI (SequenceA_Sym0 :: TyFun (t (f a)) (f ()) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing SequenceA_Sym0 Source #
(SFoldable t, SingI d) => SingI (Foldr1Sym1 d t :: TyFun (t a) a -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing (Foldr1Sym1 d t) Source #
(SFoldable t, SingI d) => SingI (Foldl1Sym1 d t :: TyFun (t a) a -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing (Foldl1Sym1 d t) Source #
SFoldable t => SingI (NullSym0 :: TyFun (t a) Bool -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing NullSym0 Source #
SFoldable t => SingI (LengthSym0 :: TyFun (t a) Nat -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing LengthSym0 Source #
(SFoldable t, SEq a, SingI d) => SingI (ElemSym1 d t :: TyFun (t a) Bool -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing (ElemSym1 d t) Source #
(STraversable t, SApplicative f) => SingI (SequenceASym0 :: TyFun (t (f a)) (f (t a)) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Traversable Methods sing :: Sing SequenceASym0 Source #
(STraversable t, SMonad m) => SingI (SequenceSym0 :: TyFun (t (m a)) (m (t a)) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Traversable Methods sing :: Sing SequenceSym0 Source #
SMonadZip m => SingI (MunzipSym0 :: TyFun (m (a, b)) (m a, m b) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Monad.Zip Methods sing :: Sing MunzipSym0 Source #
SMonadZip m => SingI (MzipSym0 :: TyFun (m a) (m b ~> m (a, b)) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Monad.Zip Methods sing :: Sing MzipSym0 Source #
SingI d => SingI (ScanrSym1 d :: TyFun b ([a] ~> NonEmpty b) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods sing :: Sing (ScanrSym1 d) Source #
SingI d => SingI (ScanlSym1 d :: TyFun b ([a] ~> NonEmpty b) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods sing :: Sing (ScanlSym1 d) Source #
SingI d => SingI (UnfoldrSym1 d :: TyFun a (NonEmpty b) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods sing :: Sing (UnfoldrSym1 d) Source #
SingI d => SingI (UnfoldSym1 d :: TyFun a (NonEmpty b) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods sing :: Sing (UnfoldSym1 d) Source #
(SMonadPlus m, SingI d) => SingI (MfilterSym1 d m :: TyFun (m a) (m a) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Monad Methods sing :: Sing (MfilterSym1 d m) Source #
(SApplicative m, SingI d) => SingI (ReplicateM_Sym1 d a m :: TyFun (m a) (m ()) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Monad Methods sing :: Sing (ReplicateM_Sym1 d a m) Source #
(SApplicative m, SingI d) => SingI (ReplicateMSym1 d a m :: TyFun (m a) (m [a]) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Monad Methods sing :: Sing (ReplicateMSym1 d a m) Source #
SingI (TyCon1 (ShowType :: t -> ErrorMessage' Symbol) :: t ~> ErrorMessage' Symbol) Source #
Instance details Defined in Data.Singletons.TypeError Methods sing :: Sing (TyCon1 ShowType) Source #
(SOrd o, SingI d) => SingI (SortWithSym1 d :: TyFun (NonEmpty a) (NonEmpty a) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods sing :: Sing (SortWithSym1 d) Source #
SingI d => SingI (ZipSym1 d b :: TyFun (NonEmpty b) (NonEmpty (a, b)) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods sing :: Sing (ZipSym1 d b) Source #
(SOrd b, SingI d) => SingI (GroupAllWith1Sym1 d :: TyFun (NonEmpty a) (NonEmpty (NonEmpty a)) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods sing :: Sing (GroupAllWith1Sym1 d) Source #
(SEq b, SingI d) => SingI (GroupWith1Sym1 d :: TyFun (NonEmpty a) (NonEmpty (NonEmpty a)) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods sing :: Sing (GroupWith1Sym1 d) Source #
SingI d => SingI (MapSym1 d :: TyFun (NonEmpty a) (NonEmpty b) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods sing :: Sing (MapSym1 d) Source #
SingI (CurrySym0 :: TyFun ((a, b) ~> c) (a ~> (b ~> c)) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Tuple Methods sing :: Sing CurrySym0 Source #
SingI (UncurrySym0 :: TyFun (a ~> (b ~> c)) ((a, b) ~> c) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Tuple Methods sing :: Sing UncurrySym0 Source #
SingI d => SingI (Maybe_Sym1 d a :: TyFun (a ~> b) (Maybe a ~> b) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Maybe Methods sing :: Sing (Maybe_Sym1 d a) Source #
SingI (FlipSym0 :: TyFun (a ~> (b ~> c)) (b ~> (a ~> c)) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Base Methods sing :: Sing FlipSym0 Source #
SingI ((.@#@$) :: TyFun (b ~> c) ((a ~> b) ~> (a ~> c)) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Base Methods sing :: Sing (.@#@$) Source #
SMonad m => SingI (LiftMSym0 :: TyFun (a1 ~> r) (m a1 ~> m r) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing LiftMSym0 Source #
SMonad m => SingI ((=<<@#@$) :: TyFun (a ~> m b) (m a ~> m b) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing (=<<@#@$) Source #
SApplicative f => SingI (LiftASym0 :: TyFun (a ~> b) (f a ~> f b) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing LiftASym0 Source #
SFunctor f => SingI (FmapSym0 :: TyFun (a ~> b) (f a ~> f b) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing FmapSym0 Source #
SFunctor f => SingI ((<$>@#@$) :: TyFun (a ~> b) (f a ~> f b) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Functor Methods sing :: Sing (<$>@#@$) Source #
SingI d => SingI (d &@#@$$ b :: TyFun (a ~> b) b -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Function Methods sing :: Sing (d &@#@$$ b) Source #
SingI (OnSym0 :: TyFun (b ~> (b ~> c)) ((a ~> b) ~> (a ~> (a ~> c))) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Function Methods sing :: Sing OnSym0 Source #
SingI (ZipWithSym0 :: TyFun (a ~> (b ~> c)) ([a] ~> ([b] ~> [c])) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing ZipWithSym0 Source #
SingI (Either_Sym0 :: TyFun (a ~> c) ((b ~> c) ~> (Either a b ~> c)) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Either Methods sing :: Sing Either_Sym0 Source #
SFoldable t => SingI (ConcatMapSym0 :: TyFun (a ~> [b]) (t a ~> [b]) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing ConcatMapSym0 Source #
(SFoldable t, SMonoid m) => SingI (FoldMapSym0 :: TyFun (a ~> m) (t a ~> m) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing FoldMapSym0 Source #
SFoldable t => SingI (FoldrSym0 :: TyFun (a ~> (b ~> b)) (b ~> (t a ~> b)) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing FoldrSym0 Source #
SFoldable t => SingI (Foldr'Sym0 :: TyFun (a ~> (b ~> b)) (b ~> (t a ~> b)) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing Foldr'Sym0 Source #
SFoldable t => SingI (FoldlSym0 :: TyFun (b ~> (a ~> b)) (b ~> (t a ~> b)) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing FoldlSym0 Source #
SFoldable t => SingI (Foldl'Sym0 :: TyFun (b ~> (a ~> b)) (b ~> (t a ~> b)) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing Foldl'Sym0 Source #
(STraversable t, SMonoid m) => SingI (FoldMapDefaultSym0 :: TyFun (a ~> m) (t a ~> m) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Traversable Methods sing :: Sing FoldMapDefaultSym0 Source #
STraversable t => SingI (FmapDefaultSym0 :: TyFun (a ~> b) (t a ~> t b) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Traversable Methods sing :: Sing FmapDefaultSym0 Source #
SingI (ZipWithSym0 :: TyFun (a ~> (b ~> c)) (NonEmpty a ~> (NonEmpty b ~> NonEmpty c)) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods sing :: Sing ZipWithSym0 Source #
SMonad m => SingI ((<$!>@#@$) :: TyFun (a ~> b) (m a ~> m b) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Monad Methods sing :: Sing (<$!>@#@$) Source #
SingI x => SingI (TyCon1 ((:<>:) x) :: ErrorMessage' Symbol ~> ErrorMessage' Symbol) Source #
Instance details Defined in Data.Singletons.TypeError Methods sing :: Sing (TyCon1 ((:<>:) x)) Source #
SingI x => SingI (TyCon1 ((:$$:) x) :: ErrorMessage' Symbol ~> ErrorMessage' Symbol) Source #
Instance details Defined in Data.Singletons.TypeError Methods sing :: Sing (TyCon1 ((:$$:) x)) Source #
(SingI n1, SingI n2) => SingI ((,) n1 n2 :: (a, b)) Source #
Instance details Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing (n1, n2) Source #
(SingI n1, SingI n2) => SingI (Arg n1 n2 :: Arg a b) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods sing :: Sing (Arg0 n1 n2) Source #
SingI (TyCon2 ((,) :: a -> b -> (a, b)) :: a ~> (b ~> (a, b))) Source #
Instance details Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing (TyCon2 (,)) Source #
SingI (Tuple4Sym0 :: TyFun a (b ~> (c ~> (d ~> (a, b, c, d)))) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing Tuple4Sym0 Source #
SingI (TyCon2 ((:) :: a -> [a] -> [a]) :: a ~> ([a] ~> [a])) Source #
Instance details Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing (TyCon2 (:)) Source #
SingI d => SingI (TyCon2 ((,,) d :: b -> c -> (a, b, c)) :: b ~> (c ~> (a, b, c))) Source #
Instance details Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing (TyCon2 ((,,) d)) Source #
SingI d => SingI (Tuple3Sym1 d b c :: TyFun b (c ~> (a, b, c)) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing (Tuple3Sym1 d b c) Source #
(SingI d2, SingI d3) => SingI (TyCon2 ((,,,) d2 d3 :: c -> d1 -> (a, b, c, d1)) :: c ~> (d1 ~> (a, b, c, d1))) Source #
Instance details Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing (TyCon2 ((,,,) d2 d3)) Source #
(SingI d2, SingI d3, SingI d4) => SingI (TyCon2 ((,,,,) d2 d3 d4 :: d1 -> e -> (a, b, c, d1, e)) :: d1 ~> (e ~> (a, b, c, d1, e))) Source #
Instance details Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing (TyCon2 ((,,,,) d2 d3 d4)) Source #
(SingI d2, SingI d3, SingI d4, SingI d5) => SingI (TyCon2 ((,,,,,) d2 d3 d4 d5 :: e -> f -> (a, b, c, d1, e, f)) :: e ~> (f ~> (a, b, c, d1, e, f))) Source #
Instance details Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing (TyCon2 ((,,,,,) d2 d3 d4 d5)) Source #
(SingI d2, SingI d3, SingI d4, SingI d5, SingI d6) => SingI (TyCon2 ((,,,,,,) d2 d3 d4 d5 d6 :: f -> g -> (a, b, c, d1, e, f, g)) :: f ~> (g ~> (a, b, c, d1, e, f, g))) Source #
Instance details Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing (TyCon2 ((,,,,,,) d2 d3 d4 d5 d6)) Source #
SingI (Unzip4Sym0 :: TyFun [(a, b, c, d)] ([a], [b], [c], [d]) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing Unzip4Sym0 Source #
(SingI d1, SingI d2) => SingI (FoldrSym2 d1 d2 :: TyFun [a] b -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Base Methods sing :: Sing (FoldrSym2 d1 d2) Source #
SingI d => SingI (ZipWithSym1 d :: TyFun [a] ([b] ~> [c]) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (ZipWithSym1 d) Source #
SingI d => SingI (Zip3Sym1 d b c :: TyFun [b] ([c] ~> [(a, b, c)]) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (Zip3Sym1 d b c) Source #
(SingI d1, SingI d2) => SingI (ScanrSym2 d1 d2 :: TyFun [a] [b] -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (ScanrSym2 d1 d2) Source #
(SingI d1, SingI d2) => SingI (ScanlSym2 d1 d2 :: TyFun [a] [b] -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (ScanlSym2 d1 d2) Source #
(SingI d1, SingI d2) => SingI (ScanrSym2 d1 d2 :: TyFun [a] (NonEmpty b) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods sing :: Sing (ScanrSym2 d1 d2) Source #
(SingI d1, SingI d2) => SingI (ScanlSym2 d1 d2 :: TyFun [a] (NonEmpty b) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods sing :: Sing (ScanlSym2 d1 d2) Source #
(SingI d1, SingI d2) => SingI (Maybe_Sym2 d1 d2 :: TyFun (Maybe a) b -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Maybe Methods sing :: Sing (Maybe_Sym2 d1 d2) Source #
SingI d => SingI (UncurrySym1 d :: TyFun (a, b) c -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Tuple Methods sing :: Sing (UncurrySym1 d) Source #
SingI (TyCon2 (Arg :: a -> b -> Arg a b) :: a ~> (b ~> Arg a b)) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods sing :: Sing (TyCon2 Arg0) Source #
SingI (TyCon2 ((:\|) :: a -> [a] -> NonEmpty a) :: a ~> ([a] ~> NonEmpty a)) Source #
Instance details Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing (TyCon2 (:\|)) Source #
SingI d => SingI (CurrySym1 d :: TyFun a (b ~> c) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Tuple Methods sing :: Sing (CurrySym1 d) Source #
(SOrd a, SingI d1, SingI d2) => SingI (ComparingSym2 d1 d2 :: TyFun b Ordering -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Ord Methods sing :: Sing (ComparingSym2 d1 d2) Source #
SingI d => SingI (FlipSym1 d :: TyFun b (a ~> c) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Base Methods sing :: Sing (FlipSym1 d) Source #
(SMonad m, SingI d) => SingI (ApSym1 d :: TyFun (m a) (m b) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing (ApSym1 d) Source #
(SMonad m, SingI d) => SingI (LiftMSym1 d m :: TyFun (m a1) (m r) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing (LiftMSym1 d m) Source #
(SMonad m, SingI d) => SingI ((=<<@#@$$) d :: TyFun (m a) (m b) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing ((=<<@#@$$) d) Source #
(SApplicative f, SingI d) => SingI (LiftASym1 d f :: TyFun (f a) (f b) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing (LiftASym1 d f) Source #
(SApplicative f, SingI d) => SingI (d <**>@#@$$ b :: TyFun (f (a ~> b)) (f b) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing (d <**>@#@$$ b) Source #
(SFunctor f, SingI d) => SingI (FmapSym1 d f :: TyFun (f a) (f b) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing (FmapSym1 d f) Source #
(SFunctor f, SingI d) => SingI ((d <$@#@$$ b) f :: TyFun (f b) (f a) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing ((d <$@#@$$ b) f) Source #
(SApplicative f, SingI d) => SingI ((<*>@#@$$) d :: TyFun (f a) (f b) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing ((<*>@#@$$) d) Source #
SApplicative f => SingI ((*>@#@$) :: TyFun (f a) (f b ~> f b) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing (*>@#@$) Source #
SApplicative f => SingI ((<*@#@$) :: TyFun (f a) (f b ~> f a) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing (<*@#@$) Source #
SMonad m => SingI ((>>@#@$) :: TyFun (m a) (m b ~> m b) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing (>>@#@$) Source #
(SAlternative f, SingI d) => SingI ((<\|>@#@$$) d :: TyFun (f a) (f a) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing ((<\|>@#@$$) d) Source #
(SMonadPlus m, SingI d) => SingI (MplusSym1 d :: TyFun (m a) (m a) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing (MplusSym1 d) Source #
(SFunctor f, SingI d) => SingI (d $>@#@$$ b :: TyFun b (f b) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Functor Methods sing :: Sing (d $>@#@$$ b) Source #
(SFunctor f, SingI d) => SingI (d <$>@#@$$ f :: TyFun (f a) (f b) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Functor Methods sing :: Sing (d <$>@#@$$ f) Source #
(SFoldable t, SingI d) => SingI (ConcatMapSym1 d t :: TyFun (t a) [b] -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing (ConcatMapSym1 d t) Source #
(SFoldable t, SMonadPlus m) => SingI (MsumSym0 :: TyFun (t (m a)) (m a) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing MsumSym0 Source #
(SFoldable t, SAlternative f) => SingI (AsumSym0 :: TyFun (t (f a)) (f a) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing AsumSym0 Source #
(SFoldable t, SMonad m) => SingI (ForM_Sym0 :: TyFun (t a) ((a ~> m b) ~> m ()) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing ForM_Sym0 Source #
(SFoldable t, SApplicative f) => SingI (For_Sym0 :: TyFun (t a) ((a ~> f b) ~> f ()) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing For_Sym0 Source #
(SFoldable t, SMonoid m, SingI d) => SingI (FoldMapSym1 d t :: TyFun (t a) m -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing (FoldMapSym1 d t) Source #
(SFoldable t, SingI d) => SingI (FoldrSym1 d t :: TyFun b (t a ~> b) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing (FoldrSym1 d t) Source #
(SFoldable t, SingI d) => SingI (Foldr'Sym1 d t :: TyFun b (t a ~> b) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing (Foldr'Sym1 d t) Source #
(SFoldable t, SingI d) => SingI (FoldlSym1 d t :: TyFun b (t a ~> b) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing (FoldlSym1 d t) Source #
(SFoldable t, SingI d) => SingI (Foldl'Sym1 d t :: TyFun b (t a ~> b) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing (Foldl'Sym1 d t) Source #
(STraversable t, SMonoid m, SingI d) => SingI (FoldMapDefaultSym1 d t :: TyFun (t a) m -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Traversable Methods sing :: Sing (FoldMapDefaultSym1 d t) Source #
(STraversable t, SingI d) => SingI (FmapDefaultSym1 d t :: TyFun (t a) (t b) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Traversable Methods sing :: Sing (FmapDefaultSym1 d t) Source #
(STraversable t, SMonad m) => SingI (ForMSym0 :: TyFun (t a) ((a ~> m b) ~> m (t b)) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Traversable Methods sing :: Sing ForMSym0 Source #
(STraversable t, SApplicative f) => SingI (ForSym0 :: TyFun (t a) ((a ~> f b) ~> f (t b)) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Traversable Methods sing :: Sing ForSym0 Source #
(SMonadZip m, SingI d) => SingI (MzipSym1 d b :: TyFun (m b) (m (a, b)) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Monad.Zip Methods sing :: Sing (MzipSym1 d b) Source #
(SMonad m, SingI d) => SingI (d <$!>@#@$$ m :: TyFun (m a) (m b) -> Type) Source #
Ins