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
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

type family Sing :: k -> Type
newtype SLambda (f :: k1 ~> k2) = SLambda {
- applySing :: forall t. Sing t -> Sing (f @@ t)
}
(@@) :: 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)
newtype WrappedSing :: forall k. k -> Type where
- WrapSing :: forall k (a :: k). {..} -> WrappedSing a
newtype SWrappedSing :: forall k (a :: k). WrappedSing a -> Type where
- SWrapSing :: forall k (a :: k) (ws :: WrappedSing a). {..} -> SWrappedSing ws
type family UnwrapSing (ws :: WrappedSing a) :: Sing a where ...
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) = Proxy
data DemoteSym0 :: (~>) Type Type
type DemoteSym1 (k6989586621679027542 :: Type) = Demote k6989586621679027542
data SameKindSym0 a6989586621679027548
data SameKindSym1 (a6989586621679027548 :: k6989586621679027547) b6989586621679027549
type SameKindSym2 (a6989586621679027548 :: k6989586621679027547) (b6989586621679027549 :: k6989586621679027547) = SameKind a6989586621679027548 b6989586621679027549
data KindOfSym0 a6989586621679027551
type KindOfSym1 (a6989586621679027551 :: k6989586621679027550) = KindOf a6989586621679027551
data (~>@#@$) a6989586621679025621
data (a6989586621679025621 :: Type) ~>@#@$$ b6989586621679025622
type (~>@#@$$$) (a6989586621679025621 :: Type) (b6989586621679025622 :: Type) = (~>) a6989586621679025621 b6989586621679025622
data ApplySym0 :: forall k16989586621679025617 k26989586621679025618. (~>) ((~>) k16989586621679025617 k26989586621679025618) ((~>) k16989586621679025617 k26989586621679025618)
data ApplySym1 (f6989586621679025619 :: (~>) k16989586621679025617 k26989586621679025618) :: (~>) k16989586621679025617 k26989586621679025618
type ApplySym2 (f6989586621679025619 :: (~>) k16989586621679025617 k26989586621679025618) (x6989586621679025620 :: k16989586621679025617) = Apply f6989586621679025619 x6989586621679025620
data (@@@#@$) a6989586621679025615
data (a6989586621679025615 :: (~>) k16989586621679032495 k6989586621679032494) @@@#@$$ b6989586621679025616
type (@@@#@$$$) (a6989586621679025615 :: (~>) k16989586621679032495 k6989586621679032494) (b6989586621679025616 :: k16989586621679032495) = (@@) a6989586621679025615 b6989586621679025616

Main singleton definitions

type family Sing :: k -> Type Source #

The singleton kind-indexed type family.

Instances

Instances details

type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = SBool
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = SOrdering
type Sing Source #
Instance details Defined in Data.Singletons.TypeLits.Internal type Sing = SNat
type Sing Source #
Instance details Defined in Data.Singletons.TypeLits.Internal type Sing = SSymbol
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = STuple0
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = SVoid
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type Sing = SAll
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type Sing = SAny
type Sing Source #
Instance details Defined in Data.Singletons.TypeError type Sing = SErrorMessage
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = SList :: [a] -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = SMaybe :: Maybe a -> Type
type Sing 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` 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 type Sing = TypeRep :: TYPE rep -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type Sing = SMin :: Min a -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type Sing = SMax :: Max a -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type Sing = SFirst :: First a -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type Sing = SLast :: Last a -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type Sing = SWrappedMonoid :: WrappedMonoid m -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type Sing = SOption :: Option a -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = SIdentity :: Identity a -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Monoid type Sing = SFirst :: First a -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Monoid type Sing = SLast :: Last a -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type Sing = SDual :: Dual a -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type Sing = SSum :: Sum a -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type Sing = SProduct :: Product a -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Ord type Sing = SDown :: Down a -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = SNonEmpty :: NonEmpty a -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = SEither :: Either a b -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = STuple2 :: (a, b) -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup type Sing = SArg :: Arg a b -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Internal type Sing = SLambda :: (k1 ~> k2) -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Internal type Sing = SWrappedSing :: WrappedSing a -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Sigma type Sing = SSigma :: Sigma s t -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = STuple3 :: (a, b, c) -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Const type Sing = SConst :: Const a b -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = STuple4 :: (a, b, c, d) -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = STuple5 :: (a, b, c, d, e) -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = STuple6 :: (a, b, c, d, e, f) -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = STuple7 :: (a, b, c, d, e, f, g) -> Type

newtype SLambda (f :: k1 ~> k2) Source #

Constructors

SLambda
Fields applySing :: forall t. Sing t -> Sing (f @@ t)

(@@) :: 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

Instances details

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 ShowSpaceSym0 Source #
Instance details Defined in Data.Singletons.Prelude.Show Methods sing :: Sing ShowSpaceSym0 Source #
SingI ShowCommaSpaceSym0 Source #
Instance details Defined in Data.Singletons.Prelude.Show Methods sing :: Sing ShowCommaSpaceSym0 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 b6989586621681331115 -> 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 (LastSym0 :: TyFun a (Last a) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Methods sing :: Sing LastSym0 Source #
SingI (FirstSym0 :: TyFun a (First a) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Methods sing :: Sing FirstSym0 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 (WrapMonoidSym0 :: TyFun m (WrappedMonoid m) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Methods sing :: Sing WrapMonoidSym0 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 (ConstSym0 :: TyFun a6989586621679097555 (Const a6989586621679097555 b6989586621679097556) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Const Methods sing :: Sing ConstSym0 Source #
(forall (a :: k). SingI a => SingI (f a), (ApplyTyCon :: (k -> k_last) -> k ~> k_last) ~ (ApplyTyConAux1 :: (k -> k_last) -> TyFun k k_last -> Type)) => SingI (TyCon1 f :: k ~> k_last) Source #
Instance details Defined in Data.Singletons Methods sing :: Sing (TyCon1 f) 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 (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 (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 (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 #
SMonadFail m => SingI (FailSym0 :: TyFun [Char] (m a) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Monad.Fail Methods sing :: Sing FailSym0 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 (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 #
(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 #
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 #
(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 m a :: TyFun (m a) (m ()) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Monad Methods sing :: Sing (ReplicateM_Sym1 d m a) Source #
(SApplicative m, SingI d) => SingI (ReplicateMSym1 d m a :: TyFun (m a) (m [a]) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Monad Methods sing :: Sing (ReplicateMSym1 d m a) 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 a => SingI ('WrapSing s :: WrappedSing a) Source #
Instance details Defined in Data.Singletons.Internal Methods sing :: Sing ('WrapSing s) Source #
(forall (a1 :: k2) (a2 :: k1). (SingI a1, SingI a2) => SingI (f a1 a2), (ApplyTyCon :: (k1 -> k_last) -> k1 ~> k_last) ~ (ApplyTyConAux1 :: (k1 -> k_last) -> TyFun k1 k_last -> Type)) => SingI (TyCon2 f :: k2 ~> (k1 ~> k_last)) Source #
Instance details Defined in Data.Singletons Methods sing :: Sing (TyCon2 f) 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 (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 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 (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 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 <$@#@$$ f) b :: TyFun (f b) (f a) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing ((d <$@#@$$ f) b) 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 #
Instance details Defined in Data.Singletons.Prelude.Monad Methods sing :: Sing (d <$!>@#@$$ m) Source #
SingI d => SingI (ZipWithSym1 d :: TyFun (NonEmpty a) (NonEmpty b ~> NonEmpty c) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods sing :: Sing (ZipWithSym1 d) Source #
SingI d => SingI (d .@#@$$ a :: TyFun (a ~> b) (a ~> c) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Base Methods sing :: Sing (d .@#@$$ a) Source #
SMonad m => SingI (LiftM2Sym0 :: TyFun (a1 ~> (a2 ~> r)) (m a1 ~> (m a2 ~> m r)) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing LiftM2Sym0 Source #
SApplicative f => SingI (LiftA2Sym0 :: TyFun (a ~> (b ~> c)) (f a ~> (f b ~> f c)) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing LiftA2Sym0 Source #
(SMonad m, SingI d) => SingI (d >>=@#@$$ b :: TyFun (a ~> m b) (m b) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing (d >>=@#@$$ b) Source #
(SFunctor f, SingI d) => SingI (d <&>@#@$$ b :: TyFun (a ~> b) (f b) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Functor Methods sing :: Sing (d <&>@#@$$ b) Source #
SingI d => SingI (OnSym1 d a :: TyFun (a ~> b) (a ~> (a ~> c)) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Function Methods sing :: Sing (OnSym1 d a) Source #
SingI (ZipWith3Sym0 :: TyFun (a ~> (b ~> (c ~> d))) ([a] ~> ([b] ~> ([c] ~> [d]))) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing ZipWith3Sym0 Source #
SingI d => SingI (Either_Sym1 d b :: TyFun (b ~> c) (Either a b ~> c) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Either Methods sing :: Sing (Either_Sym1 d b) Source #
(SFoldable t, SMonad m) => SingI (MapM_Sym0 :: TyFun (a ~> m b) (t a ~> m ()) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing MapM_Sym0 Source #
(SFoldable t, SApplicative f) => SingI (Traverse_Sym0 :: TyFun (a ~> f b) (t a ~> f ()) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing Traverse_Sym0 Source #
(SFoldable t, SMonad m) => SingI (FoldlMSym0 :: TyFun (b ~> (a ~> m b)) (b ~> (t a ~> m b)) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing FoldlMSym0 Source #
(SFoldable t, SMonad m) => SingI (FoldrMSym0 :: TyFun (a ~> (b ~> m b)) (b ~> (t a ~> m b)) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing FoldrMSym0 Source #
(STraversable t, SApplicative f) => SingI (TraverseSym0 :: TyFun (a ~> f b) (t a ~> f (t b)) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Traversable Methods sing :: Sing TraverseSym0 Source #
(STraversable t, SMonad m) => SingI (MapMSym0 :: TyFun (a ~> m b) (t a ~> m (t b)) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Traversable Methods sing :: Sing MapMSym0 Source #
STraversable t => SingI (MapAccumRSym0 :: TyFun (a ~> (b ~> (a, c))) (a ~> (t b ~> (a, t c))) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Traversable Methods sing :: Sing MapAccumRSym0 Source #
STraversable t => SingI (MapAccumLSym0 :: TyFun (a ~> (b ~> (a, c))) (a ~> (t b ~> (a, t c))) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Traversable Methods sing :: Sing MapAccumLSym0 Source #
SMonadZip m => SingI (MzipWithSym0 :: TyFun (a ~> (b ~> c)) (m a ~> (m b ~> m c)) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Monad.Zip Methods sing :: Sing MzipWithSym0 Source #
SApplicative m => SingI (ZipWithM_Sym0 :: TyFun (a ~> (b ~> m c)) ([a] ~> ([b] ~> m ())) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Monad Methods sing :: Sing ZipWithM_Sym0 Source #
SApplicative m => SingI (ZipWithMSym0 :: TyFun (a ~> (b ~> m c)) ([a] ~> ([b] ~> m [c])) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Monad Methods sing :: Sing ZipWithMSym0 Source #
SApplicative m => SingI (MapAndUnzipMSym0 :: TyFun (a ~> m (b, c)) ([a] ~> m ([b], [c])) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Monad Methods sing :: Sing MapAndUnzipMSym0 Source #
SMonad m => SingI ((<=<@#@$) :: TyFun (b ~> m c) ((a ~> m b) ~> (a ~> m c)) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Monad Methods sing :: Sing (<=<@#@$) Source #
SMonad m => SingI ((>=>@#@$) :: TyFun (a ~> m b) ((b ~> m c) ~> (a ~> m c)) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Monad Methods sing :: Sing (>=>@#@$) Source #
(forall (a1 :: k2) (a2 :: k3) (a3 :: k1). (SingI a1, SingI a2, SingI a3) => SingI (f a1 a2 a3), (ApplyTyCon :: (k1 -> k_last) -> k1 ~> k_last) ~ (ApplyTyConAux1 :: (k1 -> k_last) -> TyFun k1 k_last -> Type)) => SingI (TyCon3 f :: k2 ~> (k3 ~> (k1 ~> k_last))) Source #
Instance details Defined in Data.Singletons Methods sing :: Sing (TyCon3 f) Source #
SingI (Tuple5Sym0 :: TyFun a (b ~> (c ~> (d ~> (e ~> (a, b, c, d, e))))) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing Tuple5Sym0 Source #
SingI d2 => SingI (Tuple4Sym1 d2 b c d1 :: TyFun b (c ~> (d1 ~> (a, b, c, d1))) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing (Tuple4Sym1 d2 b c d1) Source #
(SingI d1, SingI d2) => SingI (Tuple3Sym2 d1 d2 c :: TyFun c (a, b, c) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing (Tuple3Sym2 d1 d2 c) Source #
SingI (Unzip5Sym0 :: TyFun [(a, b, c, d, e)] ([a], [b], [c], [d], [e]) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing Unzip5Sym0 Source #
SingI d2 => SingI (ZipWith3Sym1 d2 :: TyFun [a] ([b] ~> ([c] ~> [d1])) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (ZipWith3Sym1 d2) Source #
(SingI d1, SingI d2) => SingI (ZipWithSym2 d1 d2 :: TyFun [b] [c] -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (ZipWithSym2 d1 d2) Source #
(SingI d1, SingI d2) => SingI (Zip3Sym2 d1 d2 c :: TyFun [c] [(a, b, c)] -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (Zip3Sym2 d1 d2 c) Source #
(SApplicative m, SingI d) => SingI (ZipWithM_Sym1 d :: TyFun [a] ([b] ~> m ()) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Monad Methods sing :: Sing (ZipWithM_Sym1 d) Source #
(SApplicative m, SingI d) => SingI (ZipWithMSym1 d :: TyFun [a] ([b] ~> m [c]) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Monad Methods sing :: Sing (ZipWithMSym1 d) Source #
(SApplicative m, SingI d) => SingI (MapAndUnzipMSym1 d :: TyFun [a] (m ([b], [c])) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Monad Methods sing :: Sing (MapAndUnzipMSym1 d) Source #
(SingI d1, SingI d2) => SingI (Either_Sym2 d1 d2 :: TyFun (Either a b) c -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Either Methods sing :: Sing (Either_Sym2 d1 d2) Source #
(SingI d1, SingI d2) => SingI (CurrySym2 d1 d2 :: TyFun b c -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Tuple Methods sing :: Sing (CurrySym2 d1 d2) Source #
(SingI d1, SingI d2) => SingI (FlipSym2 d1 d2 :: TyFun a c -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Base Methods sing :: Sing (FlipSym2 d1 d2) Source #
(SingI d1, SingI d2) => SingI (d1 .@#@$$$ d2 :: TyFun a c -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Base Methods sing :: Sing (d1 .@#@$$$ d2) Source #
(SMonad m, SingI d) => SingI (LiftM2Sym1 d m :: TyFun (m a1) (m a2 ~> m r) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing (LiftM2Sym1 d m) Source #
(SApplicative f, SingI d) => SingI (LiftA2Sym1 d f :: TyFun (f a) (f b ~> f c) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing (LiftA2Sym1 d f) Source #
(SApplicative f, SingI d) => SingI (d *>@#@$$ b :: TyFun (f b) (f b) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing (d *>@#@$$ b) Source #
(SApplicative f, SingI d) => SingI (d <*@#@$$ b :: TyFun (f b) (f a) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing (d <*@#@$$ b) Source #
(SMonad m, SingI d) => SingI (d >>@#@$$ b :: TyFun (m b) (m b) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing (d >>@#@$$ b) Source #
(SingI d1, SingI d2) => SingI (OnSym2 d1 d2 :: TyFun a (a ~> c) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Function Methods sing :: Sing (OnSym2 d1 d2) Source #
(SFoldable t, SMonad m, SingI d) => SingI (MapM_Sym1 d t :: TyFun (t a) (m ()) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing (MapM_Sym1 d t) Source #
(SFoldable t, SApplicative f, SingI d) => SingI (Traverse_Sym1 d t :: TyFun (t a) (f ()) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing (Traverse_Sym1 d t) Source #
(SFoldable t, SMonad m, SingI d) => SingI (FoldlMSym1 d t :: TyFun b (t a ~> m b) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing (FoldlMSym1 d t) Source #
(SFoldable t, SMonad m, SingI d) => SingI (FoldrMSym1 d t :: TyFun b (t a ~> m b) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing (FoldrMSym1 d t) Source #
(SFoldable t, SingI d1, SingI d2) => SingI (FoldrSym2 d1 d2 t :: TyFun (t a) b -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing (FoldrSym2 d1 d2 t) Source #
(SFoldable t, SingI d1, SingI d2) => SingI (Foldr'Sym2 d1 d2 t :: TyFun (t a) b -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing (Foldr'Sym2 d1 d2 t) Source #
(SFoldable t, SingI d1, SingI d2) => SingI (FoldlSym2 d1 d2 t :: TyFun (t a) b -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing (FoldlSym2 d1 d2 t) Source #
(SFoldable t, SingI d1, SingI d2) => SingI (Foldl'Sym2 d1 d2 t :: TyFun (t a) b -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing (Foldl'Sym2 d1 d2 t) Source #
(STraversable t, SApplicative f, SingI d) => SingI (TraverseSym1 d t :: TyFun (t a) (f (t b)) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Traversable Methods sing :: Sing (TraverseSym1 d t) Source #
(STraversable t, SMonad m, SingI d) => SingI (MapMSym1 d t :: TyFun (t a) (m (t b)) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Traversable Methods sing :: Sing (MapMSym1 d t) Source #
(STraversable t, SingI d) => SingI (MapAccumRSym1 d t :: TyFun a (t b ~> (a, t c)) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Traversable Methods sing :: Sing (MapAccumRSym1 d t) Source #
(STraversable t, SingI d) => SingI (MapAccumLSym1 d t :: TyFun a (t b ~> (a, t c)) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Traversable Methods sing :: Sing (MapAccumLSym1 d t) Source #
(SMonadZip m, SingI d) => SingI (MzipWithSym1 d m :: TyFun (m a) (m b ~> m c) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Monad.Zip Methods sing :: Sing (MzipWithSym1 d m) Source #
(SingI d1, SingI d2) => SingI (ZipWithSym2 d1 d2 :: TyFun (NonEmpty b) (NonEmpty c) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods sing :: Sing (ZipWithSym2 d1 d2) Source #
SMonad m => SingI (LiftM3Sym0 :: TyFun (a1 ~> (a2 ~> (a3 ~> r))) (m a1 ~> (m a2 ~> (m a3 ~> m r))) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing LiftM3Sym0 Source #
SApplicative f => SingI (LiftA3Sym0 :: TyFun (a ~> (b ~> (c ~> d))) (f a ~> (f b ~> (f c ~> f d))) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing LiftA3Sym0 Source #
(SFoldable t, SMonad m, SingI d) => SingI (ForM_Sym1 d m b :: TyFun (a ~> m b) (m ()) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing (ForM_Sym1 d m b) Source #
(SFoldable t, SApplicative f, SingI d) => SingI (For_Sym1 d f b :: TyFun (a ~> f b) (f ()) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing (For_Sym1 d f b) Source #
(STraversable t, SMonad m, SingI d) => SingI (ForMSym1 d m b :: TyFun (a ~> m b) (m (t b)) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Traversable Methods sing :: Sing (ForMSym1 d m b) Source #
(STraversable t, SApplicative f, SingI d) => SingI (ForSym1 d f b :: TyFun (a ~> f b) (f (t b)) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Traversable Methods sing :: Sing (ForSym1 d f b) Source #
(SMonad m, SingI d) => SingI (d <=<@#@$$ a :: TyFun (a ~> m b) (a ~> m c) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Monad Methods sing :: Sing (d <=<@#@$$ a) Source #
(SMonad m, SingI d) => SingI (d >=>@#@$$ c :: TyFun (b ~> m c) (a ~> m c) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Monad Methods sing :: Sing (d >=>@#@$$ c) Source #
(SingI fst, SingI b) => SingI (a :&: b :: Sigma s t) Source #
Instance details Defined in Data.Singletons.Sigma Methods sing :: Sing (a :&: b) Source #
(forall (a1 :: k2) (a2 :: k3) (a3 :: k4) (a4 :: k1). (SingI a1, SingI a2, SingI a3, SingI a4) => SingI (f a1 a2 a3 a4), (ApplyTyCon :: (k1 -> k_last) -> k1 ~> k_last) ~ (ApplyTyConAux1 :: (k1 -> k_last) -> TyFun k1 k_last -> Type)) => SingI (TyCon4 f :: k2 ~> (k3 ~> (k4 ~> (k1 ~> k_last)))) Source #
Instance details Defined in Data.Singletons Methods sing :: Sing (TyCon4 f) Source #
SingI (Tuple6Sym0 :: TyFun a (b ~> (c ~> (d ~> (e ~> (f ~> (a, b, c, d, e, f)))))) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing Tuple6Sym0 Source #
SingI d2 => SingI (Tuple5Sym1 d2 b c d1 e :: TyFun b (c ~> (d1 ~> (e ~> (a, b, c, d1, e)))) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing (Tuple5Sym1 d2 b c d1 e) Source #
(SingI d2, SingI d3) => SingI (Tuple4Sym2 d2 d3 c d1 :: TyFun c (d1 ~> (a, b, c, d1)) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing (Tuple4Sym2 d2 d3 c d1) Source #
SingI (Unzip6Sym0 :: TyFun [(a, b, c, d, e, f)] ([a], [b], [c], [d], [e], [f]) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing Unzip6Sym0 Source #
(SingI d2, SingI d3) => SingI (ZipWith3Sym2 d2 d3 :: TyFun [b] ([c] ~> [d1]) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (ZipWith3Sym2 d2 d3) Source #
(SApplicative m, SingI d1, SingI d2) => SingI (ZipWithM_Sym2 d1 d2 :: TyFun [b] (m ()) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Monad Methods sing :: Sing (ZipWithM_Sym2 d1 d2) Source #
(SApplicative m, SingI d1, SingI d2) => SingI (ZipWithMSym2 d1 d2 :: TyFun [b] (m [c]) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Monad Methods sing :: Sing (ZipWithMSym2 d1 d2) Source #
(SMonad m, SingI d) => SingI (LiftM3Sym1 d m :: TyFun (m a1) (m a2 ~> (m a3 ~> m r)) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing (LiftM3Sym1 d m) Source #
(SMonad m, SingI d1, SingI d2) => SingI (LiftM2Sym2 d1 d2 :: TyFun (m a2) (m r) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing (LiftM2Sym2 d1 d2) Source #
(SApplicative f, SingI d2) => SingI (LiftA3Sym1 d2 f :: TyFun (f a) (f b ~> (f c ~> f d1)) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing (LiftA3Sym1 d2 f) Source #
(SApplicative f, SingI d1, SingI d2) => SingI (LiftA2Sym2 d1 d2 :: TyFun (f b) (f c) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing (LiftA2Sym2 d1 d2) Source #
(SingI d1, SingI d2, SingI d3) => SingI (OnSym3 d1 d2 d3 :: TyFun a c -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Function Methods sing :: Sing (OnSym3 d1 d2 d3) Source #
(SFoldable t, SMonad m, SingI d1, SingI d2) => SingI (FoldlMSym2 d1 d2 t :: TyFun (t a) (m b) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing (FoldlMSym2 d1 d2 t) Source #
(SFoldable t, SMonad m, SingI d1, SingI d2) => SingI (FoldrMSym2 d1 d2 t :: TyFun (t a) (m b) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing (FoldrMSym2 d1 d2 t) Source #
(STraversable t, SingI d1, SingI d2) => SingI (MapAccumRSym2 d1 d2 t :: TyFun (t b) (a, t c) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Traversable Methods sing :: Sing (MapAccumRSym2 d1 d2 t) Source #
(STraversable t, SingI d1, SingI d2) => SingI (MapAccumLSym2 d1 d2 t :: TyFun (t b) (a, t c) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Traversable Methods sing :: Sing (MapAccumLSym2 d1 d2 t) Source #
(SMonadZip m, SingI d1, SingI d2) => SingI (MzipWithSym2 d1 d2 :: TyFun (m b) (m c) ->