named-sop-0.1.0.0: Dependently-typed sums and products, tagged by field name

Safe HaskellNone
LanguageHaskell2010

Data.NamedSOP.Type

Contents

Description

End users should not have to manually import this module, since it is re-exported by Data.NamedSOP.Map and Data.NamedSOP.Sum.

In addition to Mapping and its related singletons, various type families related to lists are redefined here, since the ones in Data.Singletons.Prelude.List use local definitions. As of 2019-07, it is not possible to prove around local definitions that are promoted with singletons, so we are stuck redefining them.

Synopsis
  • data Mapping k v = k :-> v
  • type SMapping = (Sing :: Mapping k v -> Type)
  • type family Union (a :: [a]) (a :: [a]) :: [a] where ...
  • sUnion :: forall a (t :: [a]) (t :: [a]). SOrd a => Sing t -> Sing t -> Sing (Apply (Apply UnionSym0 t) t :: [a])
  • union :: Ord a => [a] -> [a] -> [a]
  • type family (a :: [a]) ++ (a :: [a]) :: [a] where ...
  • (%++) :: forall a (t :: [a]) (t :: [a]). Sing t -> Sing t -> Sing (Apply (Apply (++@#@$) t) t :: [a])
  • type family Insert (a :: a) (a :: [a]) :: [a] where ...
  • sInsert :: forall a (t :: a) (t :: [a]). SOrd a => Sing t -> Sing t -> Sing (Apply (Apply InsertSym0 t) t :: [a])
  • insert :: Ord a => a -> [a] -> [a]
  • type family Sort (a :: [a]) :: [a] where ...
  • sSort :: forall a (t :: [a]). SOrd a => Sing t -> Sing (Apply SortSym0 t :: [a])
  • sort :: Ord a => [a] -> [a]
  • class SingI (a :: k)
  • data family Sing (a :: k) :: Type

Symbol-value mappings

data Mapping k v Source #

A type v with an associated tag k. Importantly, its singleton data instance only takes a singleton for the tag k as its argmuent, and not one for the value v.

Constructors

k :-> v infixr 4 
Instances
(KnownSymbol k, Show v, Show (NSum xs)) => Show (NSum ((k :-> v) ': xs)) Source # 
Instance details

Defined in Data.NamedSOP.Sum

Methods

showsPrec :: Int -> NSum ((k :-> v) ': xs) -> ShowS #

show :: NSum ((k :-> v) ': xs) -> String #

showList :: [NSum ((k :-> v) ': xs)] -> ShowS #

Show (NSum ([] :: [Mapping Symbol Type])) Source # 
Instance details

Defined in Data.NamedSOP.Sum

Methods

showsPrec :: Int -> NSum [] -> ShowS #

show :: NSum [] -> String #

showList :: [NSum []] -> ShowS #

Eq a => Eq (Mapping a b) Source # 
Instance details

Defined in Data.NamedSOP.Type

Methods

(==) :: Mapping a b -> Mapping a b -> Bool #

(/=) :: Mapping a b -> Mapping a b -> Bool #

Ord a => Ord (Mapping a b) Source # 
Instance details

Defined in Data.NamedSOP.Type

Methods

compare :: Mapping a b -> Mapping a b -> Ordering #

(<) :: Mapping a b -> Mapping a b -> Bool #

(<=) :: Mapping a b -> Mapping a b -> Bool #

(>) :: Mapping a b -> Mapping a b -> Bool #

(>=) :: Mapping a b -> Mapping a b -> Bool #

max :: Mapping a b -> Mapping a b -> Mapping a b #

min :: Mapping a b -> Mapping a b -> Mapping a b #

(Show k, Show v) => Show (Mapping k v) Source # 
Instance details

Defined in Data.NamedSOP.Type

Methods

showsPrec :: Int -> Mapping k v -> ShowS #

show :: Mapping k v -> String #

showList :: [Mapping k v] -> ShowS #

SEq k => SEq (Mapping k v) Source # 
Instance details

Defined in Data.NamedSOP.Type

Methods

(%==) :: Sing a -> Sing b -> Sing (a == b)

(%/=) :: Sing a -> Sing b -> Sing (a /= b)

SOrd k => SOrd (Mapping k v) Source # 
Instance details

Defined in Data.NamedSOP.Type

Methods

sCompare :: Sing t1 -> Sing t2 -> Sing (Apply (Apply CompareSym0 t1) t2)

(%<) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (<@#@$) t1) t2)

(%<=) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (<=@#@$) t1) t2)

(%>) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (>@#@$) t1) t2)

(%>=) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (>=@#@$) t1) t2)

sMax :: Sing t1 -> Sing t2 -> Sing (Apply (Apply MaxSym0 t1) t2)

sMin :: Sing t1 -> Sing t2 -> Sing (Apply (Apply MinSym0 t1) t2)

PEq (Mapping k v) Source #

Equality and ordering on mappings uses only the key.

Instance details

Defined in Data.NamedSOP.Type

Associated Types

type x == y :: Bool

type x /= y :: Bool

POrd k => POrd (Mapping k v) Source # 
Instance details

Defined in Data.NamedSOP.Type

Associated Types

type Compare arg arg1 :: Ordering

type arg < arg1 :: Bool

type arg <= arg1 :: Bool

type arg > arg1 :: Bool

type arg >= arg1 :: Bool

type Max arg arg1 :: a

type Min arg arg1 :: a

SingI k2 => SingI (k2 :-> v2 :: Mapping k1 v1) Source # 
Instance details

Defined in Data.NamedSOP.Type

Methods

sing :: Sing (k2 :-> v2)

data Sing (a :: Mapping k v) Source # 
Instance details

Defined in Data.NamedSOP.Type

data Sing (a :: Mapping k v) where
type (x :: Mapping k v) /= (y :: Mapping k v) Source # 
Instance details

Defined in Data.NamedSOP.Type

type (x :: Mapping k v) /= (y :: Mapping k v) = Not (x == y)
type (arg :: Mapping k v) < (arg1 :: Mapping k v) Source # 
Instance details

Defined in Data.NamedSOP.Type

type (arg :: Mapping k v) < (arg1 :: Mapping k v) = Apply (Apply (TFHelper_6989586621679810484Sym0 :: TyFun (Mapping k v) (Mapping k v ~> Bool) -> Type) arg) arg1
type (arg :: Mapping k v) <= (arg1 :: Mapping k v) Source # 
Instance details

Defined in Data.NamedSOP.Type

type (arg :: Mapping k v) <= (arg1 :: Mapping k v) = Apply (Apply (TFHelper_6989586621679810502Sym0 :: TyFun (Mapping k v) (Mapping k v ~> Bool) -> Type) arg) arg1
type (arg :: Mapping k v) > (arg1 :: Mapping k v) Source # 
Instance details

Defined in Data.NamedSOP.Type

type (arg :: Mapping k v) > (arg1 :: Mapping k v) = Apply (Apply (TFHelper_6989586621679810520Sym0 :: TyFun (Mapping k v) (Mapping k v ~> Bool) -> Type) arg) arg1
type (arg :: Mapping k v) >= (arg1 :: Mapping k v) Source # 
Instance details

Defined in Data.NamedSOP.Type

type (arg :: Mapping k v) >= (arg1 :: Mapping k v) = Apply (Apply (TFHelper_6989586621679810538Sym0 :: TyFun (Mapping k v) (Mapping k v ~> Bool) -> Type) arg) arg1
type Max (arg :: Mapping k v) (arg1 :: Mapping k v) Source # 
Instance details

Defined in Data.NamedSOP.Type

type Max (arg :: Mapping k v) (arg1 :: Mapping k v) = Apply (Apply (Max_6989586621679810556Sym0 :: TyFun (Mapping k v) (Mapping k v ~> Mapping k v) -> Type) arg) arg1
type Min (arg :: Mapping k v) (arg1 :: Mapping k v) Source # 
Instance details

Defined in Data.NamedSOP.Type

type Min (arg :: Mapping k v) (arg1 :: Mapping k v) = Apply (Apply (Min_6989586621679810574Sym0 :: TyFun (Mapping k v) (Mapping k v ~> Mapping k v) -> Type) arg) arg1
type (k1 :-> _1 :: Mapping k v) == (k2 :-> _2 :: Mapping k v) Source # 
Instance details

Defined in Data.NamedSOP.Type

type (k1 :-> _1 :: Mapping k v) == (k2 :-> _2 :: Mapping k v) = k1 == k2
type Compare (k1 :-> _1 :: Mapping k v) (k2 :-> _2 :: Mapping k v) Source # 
Instance details

Defined in Data.NamedSOP.Type

type Compare (k1 :-> _1 :: Mapping k v) (k2 :-> _2 :: Mapping k v) = Compare k1 k2

type SMapping = (Sing :: Mapping k v -> Type) Source #

List operation singletons

Unlike the usual definition, this union does not remove duplicates, since that would make it impossible to define a union operation for sums.

type family Union (a :: [a]) (a :: [a]) :: [a] where ... Source #

Equations

Union xs ys = Apply SortSym0 (Apply (Apply (++@#@$) xs) ys) 

sUnion :: forall a (t :: [a]) (t :: [a]). SOrd a => Sing t -> Sing t -> Sing (Apply (Apply UnionSym0 t) t :: [a]) Source #

union :: Ord a => [a] -> [a] -> [a] Source #

type family (a :: [a]) ++ (a :: [a]) :: [a] where ... Source #

Equations

'[] ++ ys = ys 
((:) x xs) ++ ys = Apply (Apply (:@#@$) x) (Apply (Apply (++@#@$) xs) ys) 

(%++) :: forall a (t :: [a]) (t :: [a]). Sing t -> Sing t -> Sing (Apply (Apply (++@#@$) t) t :: [a]) Source #

type family Insert (a :: a) (a :: [a]) :: [a] where ... Source #

Equations

Insert x '[] = Apply (Apply (:@#@$) x) '[] 
Insert x ((:) y ys) = Case_6989586621679082763 x y ys (Let6989586621679082759Scrutinee_6989586621679078600Sym3 x y ys) 

sInsert :: forall a (t :: a) (t :: [a]). SOrd a => Sing t -> Sing t -> Sing (Apply (Apply InsertSym0 t) t :: [a]) Source #

insert :: Ord a => a -> [a] -> [a] Source #

type family Sort (a :: [a]) :: [a] where ... Source #

Equations

Sort '[] = '[] 
Sort ((:) x xs) = Apply (Apply InsertSym0 x) (Apply SortSym0 xs) 

sSort :: forall a (t :: [a]). SOrd a => Sing t -> Sing (Apply SortSym0 t :: [a]) Source #

sort :: Ord a => [a] -> [a] Source #

Convenience re-exports

class SingI (a :: k) #

Minimal complete definition

sing

Instances
SingI NotSym0 
Instance details

Defined in Data.Singletons.Prelude.Bool

Methods

sing :: Sing NotSym0

SingI (&&@#@$) 
Instance details

Defined in Data.Singletons.Prelude.Bool

Methods

sing :: Sing (&&@#@$)

SingI (||@#@$) 
Instance details

Defined in Data.Singletons.Prelude.Bool

Methods

sing :: Sing (||@#@$)

SingI Log2Sym0 
Instance details

Defined in Data.Singletons.TypeLits

Methods

sing :: Sing Log2Sym0

SingI (<=?@#@$) 
Instance details

Defined in Data.Singletons.TypeLits.Internal

Methods

sing :: Sing (<=?@#@$)

SingI DivSym0 
Instance details

Defined in Data.Singletons.TypeLits

Methods

sing :: Sing DivSym0

SingI ModSym0 
Instance details

Defined in Data.Singletons.TypeLits

Methods

sing :: Sing ModSym0

SingI (^@#@$) 
Instance details

Defined in Data.Singletons.TypeLits.Internal

Methods

sing :: Sing (^@#@$)

SingI AllSym0 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

sing :: Sing AllSym0

SingI AnySym0 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

sing :: Sing AnySym0

SingI ShowParenSym0 
Instance details

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing ShowParenSym0

SingI AndSym0 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing AndSym0

SingI OrSym0 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing OrSym0

SingI UnlinesSym0 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing UnlinesSym0

SingI UnwordsSym0 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing UnwordsSym0

SingI Show_tupleSym0 
Instance details

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing Show_tupleSym0

SingI ThenCmpSym0 
Instance details

Defined in Data.Singletons.Prelude.Ord

Methods

sing :: Sing ThenCmpSym0

SingI EftNatSym0 
Instance details

Defined in Data.Singletons.Prelude.Enum

Methods

sing :: Sing EftNatSym0

SingI EfdtNatSym0 
Instance details

Defined in Data.Singletons.Prelude.Enum

Methods

sing :: Sing EfdtNatSym0

SingI EfdtNatDnSym0 
Instance details

Defined in Data.Singletons.Prelude.Enum

Methods

sing :: Sing EfdtNatDnSym0

SingI EfdtNatUpSym0 
Instance details

Defined in Data.Singletons.Prelude.Enum

Methods

sing :: Sing EfdtNatUpSym0

SingI ShowCommaSpaceSym0 
Instance details

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing ShowCommaSpaceSym0

SingI ShowSpaceSym0 
Instance details

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing ShowSpaceSym0

SingI ShowCharSym0 
Instance details

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing ShowCharSym0

SingI ShowStringSym0 
Instance details

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing ShowStringSym0

SingI x => SingI ((&&@#@$$) x :: TyFun Bool Bool -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Bool

Methods

sing :: Sing ((&&@#@$$) x)

SingI x => SingI ((||@#@$$) x :: TyFun Bool Bool -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Bool

Methods

sing :: Sing ((||@#@$$) x)

SingI x => SingI ((<=?@#@$$) x :: TyFun Nat Bool -> Type) 
Instance details

Defined in Data.Singletons.TypeLits.Internal

Methods

sing :: Sing ((<=?@#@$$) x)

SingI x => SingI (DivSym1 x :: TyFun Nat Nat -> Type) 
Instance details

Defined in Data.Singletons.TypeLits

Methods

sing :: Sing (DivSym1 x)

SingI x => SingI (ModSym1 x :: TyFun Nat Nat -> Type) 
Instance details

Defined in Data.Singletons.TypeLits

Methods

sing :: Sing (ModSym1 x)

SingI x => SingI ((^@#@$$) x :: TyFun Nat Nat -> Type) 
Instance details

Defined in Data.Singletons.TypeLits.Internal

Methods

sing :: Sing ((^@#@$$) x)

SAlternative f => SingI (GuardSym0 :: TyFun Bool (f ()) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing GuardSym0

SApplicative f => SingI (WhenSym0 :: TyFun Bool (f () ~> f ()) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing WhenSym0

SingI (ListtransposeSym0 :: TyFun [[a]] [[a]] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing ListtransposeSym0

SingI (TransposeSym0 :: TyFun [[a]] [[a]] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing TransposeSym0

SingI (ConcatSym0 :: TyFun [[a]] [a] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing ConcatSym0

SingI (CatMaybesSym0 :: TyFun [Maybe a] [a] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Maybe

Methods

sing :: Sing CatMaybesSym0

SShow a => SingI (ShowListSym0 :: TyFun [a] (Symbol ~> Symbol) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing ShowListSym0

SingI (ListToMaybeSym0 :: TyFun [a] (Maybe a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Maybe

Methods

sing :: Sing ListToMaybeSym0

SingI (ListtailsSym0 :: TyFun [a] [[a]] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing ListtailsSym0

SNum a => SingI (ListsumSym0 :: TyFun [a] a -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing ListsumSym0

SOrd a => SingI (ListsortSym0 :: TyFun [a] [a] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing ListsortSym0

SingI (ListreverseSym0 :: TyFun [a] [a] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing ListreverseSym0

SNum a => SingI (ListproductSym0 :: TyFun [a] a -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing ListproductSym0

SingI (ListnullSym0 :: TyFun [a] Bool -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing ListnullSym0

SOrd a => SingI (ListminimumSym0 :: TyFun [a] a -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing ListminimumSym0

SOrd a => SingI (ListmaximumSym0 :: TyFun [a] a -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing ListmaximumSym0

SingI (ListlengthSym0 :: TyFun [a] Nat -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing ListlengthSym0

SingI (ListlastSym0 :: TyFun [a] a -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing ListlastSym0

SEq a => SingI (ListisPrefixOfSym0 :: TyFun [a] ([a] ~> Bool) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing ListisPrefixOfSym0

SingI (ListinitsSym0 :: TyFun [a] [[a]] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing ListinitsSym0

SingI (ListinitSym0 :: TyFun [a] [a] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing ListinitSym0

SingI (ListindexSym0 :: TyFun [a] (Nat ~> a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing ListindexSym0

SEq a => SingI ((\\@#@$) :: TyFun [a] ([a] ~> [a]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (\\@#@$)

SEq a => SingI (UnionSym0 :: TyFun [a] ([a] ~> [a]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing UnionSym0

SingI (TailsSym0 :: TyFun [a] [[a]] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing TailsSym0

SingI (TailSym0 :: TyFun [a] [a] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing TailSym0

SNum a => SingI (SumSym0 :: TyFun [a] a -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing SumSym0

SingI (SubsequencesSym0 :: TyFun [a] [[a]] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing SubsequencesSym0

SOrd a => SingI (SortSym0 :: TyFun [a] [a] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing SortSym0

SingI (ReverseSym0 :: TyFun [a] [a] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing ReverseSym0

SNum a => SingI (ProductSym0 :: TyFun [a] a -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing ProductSym0

SingI (PermutationsSym0 :: TyFun [a] [[a]] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing PermutationsSym0

SingI (NullSym0 :: TyFun [a] Bool -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing NullSym0

SEq a => SingI (NubSym0 :: TyFun [a] [a] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing NubSym0

SingI (NonEmptySubsequencesSym0 :: TyFun [a] [[a]] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing NonEmptySubsequencesSym0

SOrd a => SingI (MinimumSym0 :: TyFun [a] a -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing MinimumSym0

SOrd a => SingI (MaximumSym0 :: TyFun [a] a -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing MaximumSym0

SingI (LengthSym0 :: TyFun [a] Nat -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing LengthSym0

SingI (LastSym0 :: TyFun [a] a -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing LastSym0

SEq a => SingI (IsSuffixOfSym0 :: TyFun [a] ([a] ~> Bool) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing IsSuffixOfSym0

SEq a => SingI (IsPrefixOfSym0 :: TyFun [a] ([a] ~> Bool) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing IsPrefixOfSym0

SEq a => SingI (IsInfixOfSym0 :: TyFun [a] ([a] ~> Bool) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing IsInfixOfSym0

SEq a => SingI (IntersectSym0 :: TyFun [a] ([a] ~> [a]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing IntersectSym0

SingI (IntercalateSym0 :: TyFun [a] ([[a]] ~> [a]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing IntercalateSym0

SingI (InitsSym0 :: TyFun [a] [[a]] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing InitsSym0

SingI (InitSym0 :: TyFun [a] [a] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing InitSym0

SingI (HeadSym0 :: TyFun [a] a -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing HeadSym0

SEq a => SingI (GroupSym0 :: TyFun [a] [[a]] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing GroupSym0

SingI ((!!@#@$) :: TyFun [a] (Nat ~> a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (!!@#@$)

SingI ((++@#@$) :: TyFun [a] ([a] ~> [a]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Base

Methods

sing :: Sing (++@#@$)

SMonoid a => SingI (MconcatSym0 :: TyFun [a] a -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Monoid

Methods

sing :: Sing MconcatSym0

SingI (MaybeToListSym0 :: TyFun (Maybe a) [a] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Maybe

Methods

sing :: Sing MaybeToListSym0

SingI (IsNothingSym0 :: TyFun (Maybe a) Bool -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Maybe

Methods

sing :: Sing IsNothingSym0

SingI (IsJustSym0 :: TyFun (Maybe a) Bool -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Maybe

Methods

sing :: Sing IsJustSym0

SingI (FromJustSym0 :: TyFun (Maybe a) a -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Maybe

Methods

sing :: Sing FromJustSym0

SingI (OptionSym0 :: TyFun (Maybe a) (Option a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

sing :: Sing OptionSym0

SingI (LastSym0 :: TyFun (Maybe a) (Last a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Monoid

Methods

sing :: Sing LastSym0

SingI (FirstSym0 :: TyFun (Maybe a) (First a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Monoid

Methods

sing :: Sing FirstSym0

SingI d => SingI (ThenCmpSym1 d :: TyFun Ordering Ordering -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Ord

Methods

sing :: Sing (ThenCmpSym1 d)

SingI d => SingI (EftNatSym1 d :: TyFun Nat [Nat] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Enum

Methods

sing :: Sing (EftNatSym1 d)

SNum a => SingI (FromIntegerSym0 :: TyFun Nat a -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Num

Methods

sing :: Sing FromIntegerSym0

SEnum a => SingI (ToEnumSym0 :: TyFun Nat a -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Enum

Methods

sing :: Sing ToEnumSym0

SingI (ListtakeSym0 :: TyFun Nat ([a] ~> [a]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing ListtakeSym0

SingI (ListsplitAtSym0 :: TyFun Nat ([a] ~> ([a], [a])) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing ListsplitAtSym0

SingI (ListdropSym0 :: TyFun Nat ([a] ~> [a]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing ListdropSym0

SingI (TakeSym0 :: TyFun Nat ([a] ~> [a]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing TakeSym0

SingI (SplitAtSym0 :: TyFun Nat ([a] ~> ([a], [a])) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing SplitAtSym0

SingI (DropSym0 :: TyFun Nat ([a] ~> [a]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing DropSym0

SingI d => SingI (EfdtNatSym1 d :: TyFun Nat (Nat ~> [Nat]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Enum

Methods

sing :: Sing (EfdtNatSym1 d)

SingI d => SingI (EfdtNatDnSym1 d :: TyFun Nat (Nat ~> [Nat]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Enum

Methods

sing :: Sing (EfdtNatDnSym1 d)

SingI d => SingI (EfdtNatUpSym1 d :: TyFun Nat (Nat ~> [Nat]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Enum

Methods

sing :: Sing (EfdtNatUpSym1 d)

SShow a => SingI (ShowsPrecSym0 :: TyFun Nat (a ~> (Symbol ~> Symbol)) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing ShowsPrecSym0

SingI (ReplicateSym0 :: TyFun Nat (a ~> [a]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing ReplicateSym0

SingI d => SingI (ShowCharSym1 d :: TyFun Symbol Symbol -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing (ShowCharSym1 d)

SingI d => SingI (ShowStringSym1 d :: TyFun Symbol Symbol -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing (ShowStringSym1 d)

SingI d => SingI (Show_tupleSym1 d :: TyFun Symbol Symbol -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing (Show_tupleSym1 d)

SIsString a => SingI (FromStringSym0 :: TyFun Symbol a -> Type) 
Instance details

Defined in Data.Singletons.Prelude.IsString

Methods

sing :: Sing FromStringSym0

SShow a => SingI (ShowsSym0 :: TyFun a (Symbol ~> Symbol) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing ShowsSym0

SShow a => SingI (Show_Sym0 :: TyFun a Symbol -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing Show_Sym0

SNum a => SingI (SubtractSym0 :: TyFun a (a ~> a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Num

Methods

sing :: Sing SubtractSym0

SNum a => SingI (SignumSym0 :: TyFun a a -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Num

Methods

sing :: Sing SignumSym0

SNum a => SingI (NegateSym0 :: TyFun a a -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Num

Methods

sing :: Sing NegateSym0

SNum a => SingI (AbsSym0 :: TyFun a a -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Num

Methods

sing :: Sing AbsSym0

SNum a => SingI ((-@#@$) :: TyFun a (a ~> a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Num

Methods

sing :: Sing (-@#@$)

SNum a => SingI ((+@#@$) :: TyFun a (a ~> a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Num

Methods

sing :: Sing (+@#@$)

SNum a => SingI ((*@#@$) :: TyFun a (a ~> a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Num

Methods

sing :: Sing (*@#@$)

SingI (FromMaybeSym0 :: TyFun a (Maybe a ~> a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Maybe

Methods

sing :: Sing FromMaybeSym0

SingI (ListintersperseSym0 :: TyFun a ([a] ~> [a]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing ListintersperseSym0

SOrd a => SingI (ListinsertSym0 :: TyFun a ([a] ~> [a]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing ListinsertSym0

SEq a => SingI (ListelemSym0 :: TyFun a ([a] ~> Bool) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing ListelemSym0

SingI (PrependToAllSym0 :: TyFun a ([a] ~> [a]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing PrependToAllSym0

SEq a => SingI (NotElemSym0 :: TyFun a ([a] ~> Bool) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing NotElemSym0

SingI (IntersperseSym0 :: TyFun a ([a] ~> [a]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing IntersperseSym0

SOrd a => SingI (InsertSym0 :: TyFun a ([a] ~> [a]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing InsertSym0

SEq a => SingI (ElemSym0 :: TyFun a ([a] ~> Bool) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing ElemSym0

SEq a => SingI (ElemIndicesSym0 :: TyFun a ([a] ~> [Nat]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing ElemIndicesSym0

SEq a => SingI (ElemIndexSym0 :: TyFun a ([a] ~> Maybe Nat) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing ElemIndexSym0

SEq a => SingI (DeleteSym0 :: TyFun a ([a] ~> [a]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing DeleteSym0

SFoldable t => SingI (OrSym0 :: TyFun (t Bool) Bool -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing OrSym0

SFoldable t => SingI (AndSym0 :: TyFun (t Bool) Bool -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing AndSym0

SEnum a => SingI (SuccSym0 :: TyFun a a -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Enum

Methods

sing :: Sing SuccSym0

SEnum a => SingI (PredSym0 :: TyFun a a -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Enum

Methods

sing :: Sing PredSym0

SEnum a => SingI (FromEnumSym0 :: TyFun a Nat -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Enum

Methods

sing :: Sing FromEnumSym0

SEnum a => SingI (EnumFromToSym0 :: TyFun a (a ~> [a]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Enum

Methods

sing :: Sing EnumFromToSym0

SEnum a => SingI (EnumFromThenToSym0 :: TyFun a (a ~> (a ~> [a])) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Enum

Methods

sing :: Sing EnumFromThenToSym0

SingI (Bool_Sym0 :: TyFun a (a ~> (Bool ~> a)) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Bool

Methods

sing :: Sing Bool_Sym0

SingI (IdSym0 :: TyFun a a -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Base

Methods

sing :: Sing IdSym0

SingI (AsTypeOfSym0 :: TyFun a (a ~> a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Base

Methods

sing :: Sing AsTypeOfSym0

SEq a => SingI ((==@#@$) :: TyFun a (a ~> Bool) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Eq

Methods

sing :: Sing (==@#@$)

SEq a => SingI ((/=@#@$) :: TyFun a (a ~> Bool) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Eq

Methods

sing :: Sing (/=@#@$)

SingI (JustSym0 :: TyFun a (Maybe a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Instances

Methods

sing :: Sing JustSym0

SingI (IdentitySym0 :: TyFun a (Identity a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Instances

Methods

sing :: Sing IdentitySym0

SingI ((:|@#@$) :: TyFun a ([a] ~> NonEmpty a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Instances

Methods

sing :: Sing (:|@#@$)

SingI ((:@#@$) :: TyFun a ([a] ~> [a]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Instances

Methods

sing :: Sing (:@#@$)

SOrd a => SingI (MinSym0 :: TyFun a (a ~> a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Ord

Methods

sing :: Sing MinSym0

SOrd a => SingI (MaxSym0 :: TyFun a (a ~> a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Ord

Methods

sing :: Sing MaxSym0

SingI (DownSym0 :: TyFun a (Down a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Ord

Methods

sing :: Sing DownSym0

SOrd a => SingI (CompareSym0 :: TyFun a (a ~> Ordering) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Ord

Methods

sing :: Sing CompareSym0

SOrd a => SingI ((>@#@$) :: TyFun a (a ~> Bool) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Ord

Methods

sing :: Sing (>@#@$)

SOrd a => SingI ((>=@#@$) :: TyFun a (a ~> Bool) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Ord

Methods

sing :: Sing (>=@#@$)

SOrd a => SingI ((<@#@$) :: TyFun a (a ~> Bool) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Ord

Methods

sing :: Sing (<@#@$)

SOrd a => SingI ((<=@#@$) :: TyFun a (a ~> Bool) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Ord

Methods

sing :: Sing (<=@#@$)

SingI (WrapMonoidSym0 :: TyFun m (WrappedMonoid m) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

sing :: Sing WrapMonoidSym0

SingI (SumSym0 :: TyFun a (Sum a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

sing :: Sing SumSym0

SingI (ProductSym0 :: TyFun a (Product a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

sing :: Sing ProductSym0

SingI (MinSym0 :: TyFun a (Min a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

sing :: Sing MinSym0

SingI (MaxSym0 :: TyFun a (Max a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

sing :: Sing MaxSym0

SingI (LastSym0 :: TyFun a (Last a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

sing :: Sing LastSym0

SingI (FirstSym0 :: TyFun a (First a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

sing :: Sing FirstSym0

SingI (DualSym0 :: TyFun a (Dual a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

sing :: Sing DualSym0

SSemigroup a => SingI ((<>@#@$) :: TyFun a (a ~> a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

sing :: Sing (<>@#@$)

SMonoid a => SingI (MappendSym0 :: TyFun a (a ~> a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Monoid

Methods

sing :: Sing MappendSym0

SSemigroup a => SingI (SconcatSym0 :: TyFun (NonEmpty a) a -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

sing :: Sing SconcatSym0

SingI d => SingI (ShowParenSym1 d :: TyFun (Symbol ~> Symbol) (Symbol ~> Symbol) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing (ShowParenSym1 d)

SingI (ShowListWithSym0 :: TyFun (a ~> (Symbol ~> Symbol)) ([a] ~> (Symbol ~> Symbol)) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing ShowListWithSym0

SingI (ListtakeWhileSym0 :: TyFun (a ~> Bool) ([a] ~> [a]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing ListtakeWhileSym0

SingI (ListspanSym0 :: TyFun (a ~> Bool) ([a] ~> ([a], [a])) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing ListspanSym0

SingI (ListsortBySym0 :: TyFun (a ~> (a ~> Ordering)) ([a] ~> [a]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing ListsortBySym0

SingI (Listscanr1Sym0 :: TyFun (a ~> (a ~> a)) ([a] ~> [a]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing Listscanr1Sym0

SingI (ListpartitionSym0 :: TyFun (a ~> Bool) ([a] ~> ([a], [a])) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing ListpartitionSym0

SingI (ListnubBySym0 :: TyFun (a ~> (a ~> Bool)) ([a] ~> [a]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing ListnubBySym0

SingI (Listfoldr1Sym0 :: TyFun (a ~> (a ~> a)) ([a] ~> a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing Listfoldr1Sym0

SingI (Listfoldl1Sym0 :: TyFun (a ~> (a ~> a)) ([a] ~> a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing Listfoldl1Sym0

SingI (ListfilterSym0 :: TyFun (a ~> Bool) ([a] ~> [a]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing ListfilterSym0

SingI (ListdropWhileSym0 :: TyFun (a ~> Bool) ([a] ~> [a]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing ListdropWhileSym0

SingI (UnionBySym0 :: TyFun (a ~> (a ~> Bool)) ([a] ~> ([a] ~> [a])) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing UnionBySym0

SingI (TakeWhileSym0 :: TyFun (a ~> Bool) ([a] ~> [a]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing TakeWhileSym0

SingI (SpanSym0 :: TyFun (a ~> Bool) ([a] ~> ([a], [a])) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing SpanSym0

SingI (SortBySym0 :: TyFun (a ~> (a ~> Ordering)) ([a] ~> [a]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing SortBySym0

SingI (SelectSym0 :: TyFun (a ~> Bool) (a ~> (([a], [a]) ~> ([a], [a]))) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing SelectSym0

SingI (Scanr1Sym0 :: TyFun (a ~> (a ~> a)) ([a] ~> [a]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing Scanr1Sym0

SingI (Scanl1Sym0 :: TyFun (a ~> (a ~> a)) ([a] ~> [a]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing Scanl1Sym0

SingI (PartitionSym0 :: TyFun (a ~> Bool) ([a] ~> ([a], [a])) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing PartitionSym0

SingI (NubBySym0 :: TyFun (a ~> (a ~> Bool)) ([a] ~> [a]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing NubBySym0

SingI (MinimumBySym0 :: TyFun (a ~> (a ~> Ordering)) ([a] ~> a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing MinimumBySym0

SingI (MaximumBySym0 :: TyFun (a ~> (a ~> Ordering)) ([a] ~> a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing MaximumBySym0

SingI (IntersectBySym0 :: TyFun (a ~> (a ~> Bool)) ([a] ~> ([a] ~> [a])) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing IntersectBySym0

SingI (InsertBySym0 :: TyFun (a ~> (a ~> Ordering)) (a ~> ([a] ~> [a])) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing InsertBySym0

SingI (GroupBySym0 :: TyFun (a ~> (a ~> Bool)) ([a] ~> [[a]]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing GroupBySym0

SingI (Foldr1Sym0 :: TyFun (a ~> (a ~> a)) ([a] ~> a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing Foldr1Sym0

SingI (Foldl1Sym0 :: TyFun (a ~> (a ~> a)) ([a] ~> a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing Foldl1Sym0

SingI (Foldl1'Sym0 :: TyFun (a ~> (a ~> a)) ([a] ~> a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing Foldl1'Sym0

SingI (FindSym0 :: TyFun (a ~> Bool) ([a] ~> Maybe a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing FindSym0

SingI (FindIndicesSym0 :: TyFun (a ~> Bool) ([a] ~> [Nat]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing FindIndicesSym0

SingI (FindIndexSym0 :: TyFun (a ~> Bool) ([a] ~> Maybe Nat) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing FindIndexSym0

SingI (FilterSym0 :: TyFun (a ~> Bool) ([a] ~> [a]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing FilterSym0

SingI (Elem_bySym0 :: TyFun (a ~> (a ~> Bool)) (a ~> ([a] ~> Bool)) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing Elem_bySym0

SingI (DropWhileSym0 :: TyFun (a ~> Bool) ([a] ~> [a]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing DropWhileSym0

SingI (DropWhileEndSym0 :: TyFun (a ~> Bool) ([a] ~> [a]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing DropWhileEndSym0

SingI (DeleteFirstsBySym0 :: TyFun (a ~> (a ~> Bool)) ([a] ~> ([a] ~> [a])) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing DeleteFirstsBySym0

SingI (DeleteBySym0 :: TyFun (a ~> (a ~> Bool)) (a ~> ([a] ~> [a])) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing DeleteBySym0

SingI (BreakSym0 :: TyFun (a ~> Bool) ([a] ~> ([a], [a])) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing BreakSym0

SingI (AnySym0 :: TyFun (a ~> Bool) ([a] ~> Bool) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing AnySym0

SingI (AllSym0 :: TyFun (a ~> Bool) ([a] ~> Bool) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing AllSym0

SingI (UntilSym0 :: TyFun (a ~> Bool) ((a ~> a) ~> (a ~> a)) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Base

Methods

sing :: Sing UntilSym0

SingI d => SingI (IntercalateSym1 d :: TyFun [[a]] [a] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (IntercalateSym1 d)

SingI (RightsSym0 :: TyFun [Either a b] [b] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Either

Methods

sing :: Sing RightsSym0

SingI (PartitionEithersSym0 :: TyFun [Either a b] ([a], [b]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Either

Methods

sing :: Sing PartitionEithersSym0

SingI (LeftsSym0 :: TyFun [Either a b] [a] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Either

Methods

sing :: Sing LeftsSym0

SingI (ListunzipSym0 :: TyFun [(a, b)] ([a], [b]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing ListunzipSym0

SingI (UnzipSym0 :: TyFun [(a, b)] ([a], [b]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing UnzipSym0

SingI d => SingI (ShowListWithSym1 d :: TyFun [a] (Symbol ~> Symbol) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing (ShowListWithSym1 d)

SingI (ListzipSym0 :: TyFun [a] ([b] ~> [(a, b)]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing ListzipSym0

SingI d => SingI (ListtakeWhileSym1 d :: TyFun [a] [a] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing (ListtakeWhileSym1 d)

SingI d => SingI (ListtakeSym1 d a :: TyFun [a] [a] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing (ListtakeSym1 d a)

SingI d => SingI (ListsplitAtSym1 d a :: TyFun [a] ([a], [a]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing (ListsplitAtSym1 d a)

SingI d => SingI (ListspanSym1 d :: TyFun [a] ([a], [a]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing (ListspanSym1 d)

SingI d => SingI (ListsortBySym1 d :: TyFun [a] [a] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing (ListsortBySym1 d)

SingI d => SingI (Listscanr1Sym1 d :: TyFun [a] [a] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing (Listscanr1Sym1 d)

SingI d => SingI (ListpartitionSym1 d :: TyFun [a] ([a], [a]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing (ListpartitionSym1 d)

SingI d => SingI (ListnubBySym1 d :: TyFun [a] [a] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing (ListnubBySym1 d)

(SEq a, SingI d) => SingI (ListisPrefixOfSym1 d :: TyFun [a] Bool -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing (ListisPrefixOfSym1 d)

SingI d => SingI (ListintersperseSym1 d :: TyFun [a] [a] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing (ListintersperseSym1 d)

(SOrd a, SingI d) => SingI (ListinsertSym1 d :: TyFun [a] [a] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing (ListinsertSym1 d)

SingI d => SingI (Listfoldr1Sym1 d :: TyFun [a] a -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing (Listfoldr1Sym1 d)

SingI d => SingI (Listfoldl1Sym1 d :: TyFun [a] a -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing (Listfoldl1Sym1 d)

SingI d => SingI (ListfilterSym1 d :: TyFun [a] [a] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing (ListfilterSym1 d)

(SEq a, SingI d) => SingI (ListelemSym1 d :: TyFun [a] Bool -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing (ListelemSym1 d)

SingI d => SingI (ListdropWhileSym1 d :: TyFun [a] [a] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing (ListdropWhileSym1 d)

SingI d => SingI (ListdropSym1 d a :: TyFun [a] [a] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing (ListdropSym1 d a)

(SEq a, SingI d) => SingI ((\\@#@$$) d :: TyFun [a] [a] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing ((\\@#@$$) d)

SingI (ZipSym0 :: TyFun [a] ([b] ~> [(a, b)]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing ZipSym0

(SEq a, SingI d) => SingI (UnionSym1 d :: TyFun [a] [a] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (UnionSym1 d)

SingI d => SingI (UnionBySym1 d :: TyFun [a] ([a] ~> [a]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (UnionBySym1 d)

SingI d => SingI (TakeWhileSym1 d :: TyFun [a] [a] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (TakeWhileSym1 d)

SingI d => SingI (TakeSym1 d a :: TyFun [a] [a] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (TakeSym1 d a)

SingI d => SingI (SplitAtSym1 d a :: TyFun [a] ([a], [a]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (SplitAtSym1 d a)

SingI d => SingI (SpanSym1 d :: TyFun [a] ([a], [a]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (SpanSym1 d)

SingI d => SingI (SortBySym1 d :: TyFun [a] [a] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (SortBySym1 d)

SingI d => SingI (Scanr1Sym1 d :: TyFun [a] [a] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (Scanr1Sym1 d)

SingI d => SingI (Scanl1Sym1 d :: TyFun [a] [a] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (Scanl1Sym1 d)

SingI d => SingI (PrependToAllSym1 d :: TyFun [a] [a] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (PrependToAllSym1 d)

SingI d => SingI (PartitionSym1 d :: TyFun [a] ([a], [a]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (PartitionSym1 d)

SingI d => SingI (NubBySym1 d :: TyFun [a] [a] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (NubBySym1 d)

(SEq a, SingI d) => SingI (NotElemSym1 d :: TyFun [a] Bool -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (NotElemSym1 d)

SingI d => SingI (MinimumBySym1 d :: TyFun [a] a -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (MinimumBySym1 d)

SingI d => SingI (MaximumBySym1 d :: TyFun [a] a -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (MaximumBySym1 d)

(SEq a, SingI d) => SingI (IsSuffixOfSym1 d :: TyFun [a] Bool -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (IsSuffixOfSym1 d)

(SEq a, SingI d) => SingI (IsPrefixOfSym1 d :: TyFun [a] Bool -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (IsPrefixOfSym1 d)

(SEq a, SingI d) => SingI (IsInfixOfSym1 d :: TyFun [a] Bool -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (IsInfixOfSym1 d)

SingI d => SingI (IntersperseSym1 d :: TyFun [a] [a] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (IntersperseSym1 d)

(SEq a, SingI d) => SingI (IntersectSym1 d :: TyFun [a] [a] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (IntersectSym1 d)

SingI d => SingI (IntersectBySym1 d :: TyFun [a] ([a] ~> [a]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (IntersectBySym1 d)

(SOrd a, SingI d) => SingI (InsertSym1 d :: TyFun [a] [a] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (InsertSym1 d)

SingI d => SingI (GroupBySym1 d :: TyFun [a] [[a]] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (GroupBySym1 d)

SNum i => SingI (GenericLengthSym0 :: TyFun [a] i -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing GenericLengthSym0

SingI d => SingI (Foldr1Sym1 d :: TyFun [a] a -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (Foldr1Sym1 d)

SingI d => SingI (Foldl1Sym1 d :: TyFun [a] a -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (Foldl1Sym1 d)

SingI d => SingI (Foldl1'Sym1 d :: TyFun [a] a -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (Foldl1'Sym1 d)

SingI d => SingI (FindSym1 d :: TyFun [a] (Maybe a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (FindSym1 d)

SingI d => SingI (FindIndicesSym1 d :: TyFun [a] [Nat] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (FindIndicesSym1 d)

SingI d => SingI (FindIndexSym1 d :: TyFun [a] (Maybe Nat) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (FindIndexSym1 d)

SingI d => SingI (FilterSym1 d :: TyFun [a] [a] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (FilterSym1 d)

(SEq a, SingI d) => SingI (ElemSym1 d :: TyFun [a] Bool -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (ElemSym1 d)

(SEq a, SingI d) => SingI (ElemIndicesSym1 d :: TyFun [a] [Nat] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (ElemIndicesSym1 d)

(SEq a, SingI d) => SingI (ElemIndexSym1 d :: TyFun [a] (Maybe Nat) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (ElemIndexSym1 d)

SingI d => SingI (DropWhileSym1 d :: TyFun [a] [a] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (DropWhileSym1 d)

SingI d => SingI (DropWhileEndSym1 d :: TyFun [a] [a] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (DropWhileEndSym1 d)

SingI d => SingI (DropSym1 d a :: TyFun [a] [a] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (DropSym1 d a)

(SEq a, SingI d) => SingI (DeleteSym1 d :: TyFun [a] [a] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (DeleteSym1 d)

SingI d => SingI (DeleteFirstsBySym1 d :: TyFun [a] ([a] ~> [a]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (DeleteFirstsBySym1 d)

SingI d => SingI (BreakSym1 d :: TyFun [a] ([a], [a]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (BreakSym1 d)

SingI d => SingI (AnySym1 d :: TyFun [a] Bool -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (AnySym1 d)

SingI d => SingI (AllSym1 d :: TyFun [a] Bool -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (AllSym1 d)

SingI d => SingI ((++@#@$$) d :: TyFun [a] [a] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Base

Methods

sing :: Sing ((++@#@$$) d)

SingI d => SingI ((:|@#@$$) d :: TyFun [a] (NonEmpty a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Instances

Methods

sing :: Sing ((:|@#@$$) d)

SingI d => SingI ((:@#@$$) d :: TyFun [a] [a] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Instances

Methods

sing :: Sing ((:@#@$$) d)

SingI d => SingI (FromMaybeSym1 d :: TyFun (Maybe a) a -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Maybe

Methods

sing :: Sing (FromMaybeSym1 d)

SingI (IsRightSym0 :: TyFun (Either a b) Bool -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Either

Methods

sing :: Sing IsRightSym0

SingI (IsLeftSym0 :: TyFun (Either a b) Bool -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Either

Methods

sing :: Sing IsLeftSym0

(SingI d1, SingI d2) => SingI (EfdtNatSym2 d1 d2 :: TyFun Nat [Nat] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Enum

Methods

sing :: Sing (EfdtNatSym2 d1 d2)

(SingI d1, SingI d2) => SingI (EfdtNatDnSym2 d1 d2 :: TyFun Nat [Nat] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Enum

Methods

sing :: Sing (EfdtNatDnSym2 d1 d2)

(SingI d1, SingI d2) => SingI (EfdtNatUpSym2 d1 d2 :: TyFun Nat [Nat] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Enum

Methods

sing :: Sing (EfdtNatUpSym2 d1 d2)

SingI d => SingI (ListindexSym1 d :: TyFun Nat a -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing (ListindexSym1 d)

SingI d => SingI ((!!@#@$$) d :: TyFun Nat a -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing ((!!@#@$$) d)

(SingI d1, SingI d2) => SingI (ShowParenSym2 d1 d2 :: TyFun Symbol Symbol -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing (ShowParenSym2 d1 d2)

(SShow a, SingI d) => SingI (ShowListSym1 d :: TyFun Symbol Symbol -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing (ShowListSym1 d)

(SShow a, SingI d) => SingI (ShowsSym1 d :: TyFun Symbol Symbol -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing (ShowsSym1 d)

SingI (ErrorWithoutStackTraceSym0 :: TyFun Symbol a -> Type) 
Instance details

Defined in Data.Singletons.TypeLits.Internal

Methods

sing :: Sing ErrorWithoutStackTraceSym0

SingI (ErrorSym0 :: TyFun Symbol a -> Type) 
Instance details

Defined in Data.Singletons.TypeLits.Internal

Methods

sing :: Sing ErrorSym0

SingI (SwapSym0 :: TyFun (a, b) (b, a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Tuple

Methods

sing :: Sing SwapSym0

SingI (SndSym0 :: TyFun (a, b) b -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Tuple

Methods

sing :: Sing SndSym0

SingI (FstSym0 :: TyFun (a, b) a -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Tuple

Methods

sing :: Sing FstSym0

(SShow a, SingI d) => SingI (ShowsPrecSym1 d a :: TyFun a (Symbol ~> Symbol) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing (ShowsPrecSym1 d a)

(SNum a, SingI d) => SingI (SubtractSym1 d :: TyFun a a -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Num

Methods

sing :: Sing (SubtractSym1 d)

(SNum a, SingI d) => SingI ((-@#@$$) d :: TyFun a a -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Num

Methods

sing :: Sing ((-@#@$$) d)

(SNum a, SingI d) => SingI ((+@#@$$) d :: TyFun a a -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Num

Methods

sing :: Sing ((+@#@$$) d)

(SNum a, SingI d) => SingI ((*@#@$$) d :: TyFun a a -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Num

Methods

sing :: Sing ((*@#@$$) d)

(SApplicative f, SingI d) => SingI (WhenSym1 d f :: TyFun (f ()) (f ()) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing (WhenSym1 d f)

SMonad m => SingI (ReturnSym0 :: TyFun a (m a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing ReturnSym0

SApplicative f => SingI (PureSym0 :: TyFun a (f a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing PureSym0

SMonad m => SingI (JoinSym0 :: TyFun (m (m a)) (m a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing JoinSym0

SingI (Maybe_Sym0 :: TyFun b ((a ~> b) ~> (Maybe a ~> b)) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Maybe

Methods

sing :: Sing Maybe_Sym0

SingI d => SingI (SelectSym1 d :: TyFun a (([a], [a]) ~> ([a], [a])) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (SelectSym1 d)

SingI d => SingI (ReplicateSym1 d a :: TyFun a [a] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (ReplicateSym1 d a)

SEq a => SingI (LookupSym0 :: TyFun a ([(a, b)] ~> Maybe b) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing LookupSym0

SingI d => SingI (InsertBySym1 d :: TyFun a ([a] ~> [a]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (InsertBySym1 d)

SingI d => SingI (Elem_bySym1 d :: TyFun a ([a] ~> Bool) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (Elem_bySym1 d)

SingI d => SingI (DeleteBySym1 d :: TyFun a ([a] ~> [a]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (DeleteBySym1 d)

SFoldable t => SingI (ToListSym0 :: TyFun (t a) [a] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing ToListSym0

(SFoldable t, SNum a) => SingI (SumSym0 :: TyFun (t a) a -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing SumSym0

(SFoldable t, SNum a) => SingI (ProductSym0 :: TyFun (t a) a -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing ProductSym0

(SFoldable t, SEq a) => SingI (NotElemSym0 :: TyFun a (t a ~> Bool) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing NotElemSym0

(SFoldable t, SOrd a) => SingI (MinimumSym0 :: TyFun (t a) a -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing MinimumSym0

(SFoldable t, SOrd a) => SingI (MaximumSym0 :: TyFun (t a) a -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing MaximumSym0

(SFoldable t, SMonoid m) => SingI (FoldSym0 :: TyFun (t m) m -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing FoldSym0

(SFoldable t, SEq a) => SingI (ElemSym0 :: TyFun a (t a ~> Bool) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing ElemSym0

SFoldable t => SingI (ConcatSym0 :: TyFun (t [a]) [a] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing ConcatSym0

(SEnum a, SingI d) => SingI (EnumFromToSym1 d :: TyFun a [a] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Enum

Methods

sing :: Sing (EnumFromToSym1 d)

(SEnum a, SingI d) => SingI (EnumFromThenToSym1 d :: TyFun a (a ~> [a]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Enum

Methods

sing :: Sing (EnumFromThenToSym1 d)

SingI d => SingI (Bool_Sym1 d :: TyFun a (Bool ~> a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Bool

Methods

sing :: Sing (Bool_Sym1 d)

SingI (SeqSym0 :: TyFun a (b ~> b) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Base

Methods

sing :: Sing SeqSym0

SingI (ConstSym0 :: TyFun a (b ~> a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Base

Methods

sing :: Sing ConstSym0

SingI d => SingI (AsTypeOfSym1 d :: TyFun a a -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Base

Methods

sing :: Sing (AsTypeOfSym1 d)

(SEq a, SingI x) => SingI ((==@#@$$) x :: TyFun a Bool -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Eq

Methods

sing :: Sing ((==@#@$$) x)

(SEq a, SingI x) => SingI ((/=@#@$$) x :: TyFun a Bool -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Eq

Methods

sing :: Sing ((/=@#@$$) x)

SingI (Tuple2Sym0 :: TyFun a (b ~> (a, b)) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Instances

Methods

sing :: Sing Tuple2Sym0

SingI (RightSym0 :: TyFun b (Either a b) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Instances

Methods

sing :: Sing RightSym0

SingI (LeftSym0 :: TyFun a (Either a b) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Instances

Methods

sing :: Sing LeftSym0

(SOrd a, SingI d) => SingI (MinSym1 d :: TyFun a a -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Ord

Methods

sing :: Sing (MinSym1 d)

(SOrd a, SingI d) => SingI (MaxSym1 d :: TyFun a a -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Ord

Methods

sing :: Sing (MaxSym1 d)

(SOrd a, SingI d) => SingI (CompareSym1 d :: TyFun a Ordering -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Ord

Methods

sing :: Sing (CompareSym1 d)

(SOrd a, SingI d) => SingI ((>@#@$$) d :: TyFun a Bool -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Ord

Methods

sing :: Sing ((>@#@$$) d)

(SOrd a, SingI d) => SingI ((>=@#@$$) d :: TyFun a Bool -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Ord

Methods

sing :: Sing ((>=@#@$$) d)

(SOrd a, SingI d) => SingI ((<@#@$$) d :: TyFun a Bool -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Ord

Methods

sing :: Sing ((<@#@$$) d)

(SOrd a, SingI d) => SingI ((<=@#@$$) d :: TyFun a Bool -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Ord

Methods

sing :: Sing ((<=@#@$$) d)

(SSemigroup a, SingI d) => SingI ((<>@#@$$) d :: TyFun a a -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

sing :: Sing ((<>@#@$$) d)

(SMonoid a, SingI d) => SingI (MappendSym1 d :: TyFun a a -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Monoid

Methods

sing :: Sing (MappendSym1 d)

SFunctor f => SingI (VoidSym0 :: TyFun (f a) (f ()) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Functor

Methods

sing :: Sing VoidSym0

SAlternative f => SingI (OptionalSym0 :: TyFun (f a) (f (Maybe a)) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Applicative

Methods

sing :: Sing OptionalSym0

SingI (Option_Sym0 :: TyFun b ((a ~> b) ~> (Option a ~> b)) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Semigroup

Methods

sing :: Sing Option_Sym0

SingI (ArgSym0 :: TyFun a (b ~> Arg a b) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Semigroup

Methods

sing :: Sing ArgSym0

SingI (MapMaybeSym0 :: TyFun (a ~> Maybe b) ([a] ~> [b]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Maybe

Methods

sing :: Sing MapMaybeSym0

SingI (ListscanrSym0 :: TyFun (a ~> (b ~> b)) (b ~> ([a] ~> [b])) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing ListscanrSym0

SingI (ListscanlSym0 :: TyFun (b ~> (a ~> b)) (b ~> ([a] ~> [b])) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing ListscanlSym0

SingI (ListmapSym0 :: TyFun (a ~> b) ([a] ~> [b]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing ListmapSym0

SingI (ListfoldrSym0 :: TyFun (a ~> (b ~> b)) (b ~> ([a] ~> b)) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing ListfoldrSym0

SingI (ListfoldlSym0 :: TyFun (b ~> (a ~> b)) (b ~> ([a] ~> b)) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing ListfoldlSym0

SingI (Listfoldl'Sym0 :: TyFun (b ~> (a ~> b)) (b ~> ([a] ~> b)) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing Listfoldl'Sym0

SingI (UnfoldrSym0 :: TyFun (b ~> Maybe (a, b)) (b ~> [a]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing UnfoldrSym0

SingI (ScanrSym0 :: TyFun (a ~> (b ~> b)) (b ~> ([a] ~> [b])) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing ScanrSym0

SingI (ScanlSym0 :: TyFun (b ~> (a ~> b)) (b ~> ([a] ~> [b])) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing ScanlSym0

SingI (Foldl'Sym0 :: TyFun (b ~> (a ~> b)) (b ~> ([a] ~> b)) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing Foldl'Sym0

SingI (ConcatMapSym0 :: TyFun (a ~> [b]) ([a] ~> [b]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing ConcatMapSym0

SFoldable t => SingI (MinimumBySym0 :: TyFun (a ~> (a ~> Ordering)) (t a ~> a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing MinimumBySym0

SFoldable t => SingI (MaximumBySym0 :: TyFun (a ~> (a ~> Ordering)) (t a ~> a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing MaximumBySym0

SFoldable t => SingI (Foldr1Sym0 :: TyFun (a ~> (a ~> a)) (t a ~> a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing Foldr1Sym0

SFoldable t => SingI (Foldl1Sym0 :: TyFun (a ~> (a ~> a)) (t a ~> a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing Foldl1Sym0

SFoldable t => SingI (FindSym0 :: TyFun (a ~> Bool) (t a ~> Maybe a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing FindSym0

SFoldable t => SingI (AnySym0 :: TyFun (a ~> Bool) (t a ~> Bool) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing AnySym0

SFoldable t => SingI (AllSym0 :: TyFun (a ~> Bool) (t a ~> Bool) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing AllSym0

SingI d => SingI (UntilSym1 d :: TyFun (a ~> a) (a ~> a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Base

Methods

sing :: Sing (UntilSym1 d)

SingI (MapSym0 :: TyFun (a ~> b) ([a] ~> [b]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Base

Methods

sing :: Sing MapSym0

SingI (FoldrSym0 :: TyFun (a ~> (b ~> b)) (b ~> ([a] ~> b)) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Base

Methods

sing :: Sing FoldrSym0

SingI (($@#@$) :: TyFun (a ~> b) (a ~> b) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Base

Methods

sing :: Sing ($@#@$)

SingI (($!@#@$) :: TyFun (a ~> b) (a ~> b) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Base

Methods

sing :: Sing ($!@#@$)

SingI (FoldlSym0 :: TyFun (b ~> (a ~> b)) (b ~> ([a] ~> b)) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Instances

Methods

sing :: Sing FoldlSym0

SOrd a => SingI (ComparingSym0 :: TyFun (b ~> a) (b ~> (b ~> Ordering)) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Ord

Methods

sing :: Sing ComparingSym0

SingI (ConstSym0 :: TyFun a6989586621679095402 (Const a6989586621679095402 b6989586621679095403) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Const

Methods

sing :: Sing ConstSym0

(SingI d1, SingI d2) => SingI (Bool_Sym2 d1 d2 :: TyFun Bool a -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Bool

Methods

sing :: Sing (Bool_Sym2 d1 d2)

(SEq a, SingI d) => SingI (LookupSym1 d b :: TyFun [(a, b)] (Maybe b) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (LookupSym1 d b)

SingI (Unzip3Sym0 :: TyFun [(a, b, c)] ([a], [b], [c]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing Unzip3Sym0

SingI d => SingI (MapMaybeSym1 d :: TyFun [a] [b] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Maybe

Methods

sing :: Sing (MapMaybeSym1 d)

SingI d => SingI (ListzipSym1 d b :: TyFun [b] [(a, b)] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing (ListzipSym1 d b)

SingI d => SingI (ListmapSym1 d :: TyFun [a] [b] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing (ListmapSym1 d)

SingI d => SingI (ZipSym1 d b :: TyFun [b] [(a, b)] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (ZipSym1 d b)

SingI (Zip3Sym0 :: TyFun [a] ([b] ~> ([c] ~> [(a, b, c)])) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing Zip3Sym0

(SingI d1, SingI d2) => SingI (UnionBySym2 d1 d2 :: TyFun [a] [a] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (UnionBySym2 d1 d2)

(SingI d1, SingI d2) => SingI (IntersectBySym2 d1 d2 :: TyFun [a] [a] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (IntersectBySym2 d1 d2)

(SingI d1, SingI d2) => SingI (InsertBySym2 d1 d2 :: TyFun [a] [a] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (InsertBySym2 d1 d2)

(SingI d1, SingI d2) => SingI (Elem_bySym2 d1 d2 :: TyFun [a] Bool -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (Elem_bySym2 d1 d2)

(SingI d1, SingI d2) => SingI (DeleteFirstsBySym2 d1 d2 :: TyFun [a] [a] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (DeleteFirstsBySym2 d1 d2)

(SingI d1, SingI d2) => SingI (DeleteBySym2 d1 d2 :: TyFun [a] [a] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (DeleteBySym2 d1 d2)

SingI d => SingI (ConcatMapSym1 d :: TyFun [a] [b] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (ConcatMapSym1 d)

SingI d => SingI (MapSym1 d :: TyFun [a] [b] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Base

Methods

sing :: Sing (MapSym1 d)

(SShow a, SingI d1, SingI d2) => SingI (ShowsPrecSym2 d1 d2 :: TyFun Symbol Symbol -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing (ShowsPrecSym2 d1 d2)

(SingI d1, SingI d2) => SingI (ShowListWithSym2 d1 d2 :: TyFun Symbol Symbol -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing (ShowListWithSym2 d1 d2)

SMonad m => SingI (FailSym0 :: TyFun Symbol (m a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing FailSym0

(SingI d1, SingI d2) => SingI (SelectSym2 d1 d2 :: TyFun ([a], [a]) ([a], [a]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (SelectSym2 d1 d2)

(STraversable t, SMonad m) => SingI (SequenceSym0 :: TyFun (t (m a)) (m (t a)) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Traversable

Methods

sing :: Sing SequenceSym0

(STraversable t, SApplicative f) => SingI (SequenceASym0 :: TyFun (t (f a)) (f (t a)) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Traversable

Methods

sing :: Sing SequenceASym0

SMonadPlus m => SingI (MplusSym0 :: TyFun (m a) (m a ~> m a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing MplusSym0

SMonad m => SingI (ApSym0 :: TyFun (m (a ~> b)) (m a ~> m b) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing ApSym0

SMonad m => SingI ((>>=@#@$) :: TyFun (m a) ((a ~> m b) ~> m b) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing (>>=@#@$)

SAlternative f => SingI ((<|>@#@$) :: TyFun (f a) (f a ~> f a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing (<|>@#@$)

SApplicative f => SingI ((<*>@#@$) :: TyFun (f (a ~> b)) (f a ~> f b) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing (<*>@#@$)

SApplicative f => SingI ((<**>@#@$) :: TyFun (f a) (f (a ~> b) ~> f b) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing (<**>@#@$)

SFunctor f => SingI ((<$@#@$) :: TyFun a (f b ~> f a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing (<$@#@$)

SingI d => SingI (ListscanrSym1 d :: TyFun b ([a] ~> [b]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing (ListscanrSym1 d)

SingI d => SingI (ListscanlSym1 d :: TyFun b ([a] ~> [b]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing (ListscanlSym1 d)

SingI d => SingI (ListfoldrSym1 d :: TyFun b ([a] ~> b) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing (ListfoldrSym1 d)

SingI d => SingI (ListfoldlSym1 d :: TyFun b ([a] ~> b) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing (ListfoldlSym1 d)

SingI d => SingI (Listfoldl'Sym1 d :: TyFun b ([a] ~> b) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing (Listfoldl'Sym1 d)

SingI d => SingI (UnfoldrSym1 d :: TyFun b [a] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (UnfoldrSym1 d)

SingI d => SingI (ScanrSym1 d :: TyFun b ([a] ~> [b]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (ScanrSym1 d)

SingI d => SingI (ScanlSym1 d :: TyFun b ([a] ~> [b]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (ScanlSym1 d)

SingI d => SingI (Foldl'Sym1 d :: TyFun b ([a] ~> b) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (Foldl'Sym1 d)

(SFoldable t, SMonad m) => SingI (Sequence_Sym0 :: TyFun (t (m a)) (m ()) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing Sequence_Sym0

(SFoldable t, SApplicative f) => SingI (SequenceA_Sym0 :: TyFun (t (f a)) (f ()) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing SequenceA_Sym0

SFoldable t => SingI (NullSym0 :: TyFun (t a) Bool -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing NullSym0

(SFoldable t, SEq a, SingI d) => SingI (NotElemSym1 d t :: TyFun (t a) Bool -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing (NotElemSym1 d t)

(SFoldable t, SingI d) => SingI (MinimumBySym1 d t :: TyFun (t a) a -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing (MinimumBySym1 d t)

(SFoldable t, SingI d) => SingI (MaximumBySym1 d t :: TyFun (t a) a -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing (MaximumBySym1 d t)

SFoldable t => SingI (LengthSym0 :: TyFun (t a) Nat -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing LengthSym0

(SFoldable t, SingI d) => SingI (Foldr1Sym1 d t :: TyFun (t a) a -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing (Foldr1Sym1 d t)

(SFoldable t, SingI d) => SingI (Foldl1Sym1 d t :: TyFun (t a) a -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing (Foldl1Sym1 d t)

(SFoldable t, SingI d) => SingI (FindSym1 d t :: TyFun (t a) (Maybe a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing (FindSym1 d t)

(SFoldable t, SEq a, SingI d) => SingI (ElemSym1 d t :: TyFun (t a) Bool -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing (ElemSym1 d t)

(SFoldable t, SingI d) => SingI (AnySym1 d t :: TyFun (t a) Bool -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing (AnySym1 d t)

(SFoldable t, SingI d) => SingI (AllSym1 d t :: TyFun (t a) Bool -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing (AllSym1 d t)

(SEnum a, SingI d1, SingI d2) => SingI (EnumFromThenToSym2 d1 d2 :: TyFun a [a] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Enum

Methods

sing :: Sing (EnumFromThenToSym2 d1 d2)

(SingI d1, SingI d2) => SingI (UntilSym2 d1 d2 :: TyFun a a -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Base

Methods

sing :: Sing (UntilSym2 d1 d2)

SingI d => SingI (SeqSym1 d b :: TyFun b b -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Base

Methods

sing :: Sing (SeqSym1 d b)

SingI d => SingI (FoldrSym1 d :: TyFun b ([a] ~> b) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Base

Methods

sing :: Sing (FoldrSym1 d)

SingI d => SingI (ConstSym1 d b :: TyFun b a -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Base

Methods

sing :: Sing (ConstSym1 d b)

SingI d => SingI (($@#@$$) d :: TyFun a b -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Base

Methods

sing :: Sing (($@#@$$) d)

SingI d => SingI (($!@#@$$) d :: TyFun a b -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Base

Methods

sing :: Sing (($!@#@$$) d)

SingI (Tuple3Sym0 :: TyFun a (b ~> (c ~> (a, b, c))) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Instances

Methods

sing :: Sing Tuple3Sym0

SingI d => SingI (Tuple2Sym1 d b :: TyFun b (a, b) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Instances

Methods

sing :: Sing (Tuple2Sym1 d b)

SingI d => SingI (FoldlSym1 d :: TyFun b ([a] ~> b) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Instances

Methods

sing :: Sing (FoldlSym1 d)

(SOrd a, SingI d) => SingI (ComparingSym1 d :: TyFun b (b ~> Ordering) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Ord

Methods

sing :: Sing (ComparingSym1 d)

SFunctor f => SingI ((<&>@#@$) :: TyFun (f a) ((a ~> b) ~> f b) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Functor

Methods

sing :: Sing (<&>@#@$)

SFunctor f => SingI (($>@#@$) :: TyFun (f a) (b ~> f b) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Functor

Methods

sing :: Sing ($>@#@$)

SingI d => SingI (ArgSym1 d b :: TyFun b (Arg a b) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Semigroup

Methods

sing :: Sing (ArgSym1 d b)

SingI (CurrySym0 :: TyFun ((a, b) ~> c) (a ~> (b ~> c)) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Tuple

Methods

sing :: Sing CurrySym0

SingI (UncurrySym0 :: TyFun (a ~> (b ~> c)) ((a, b) ~> c) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Tuple

Methods

sing :: Sing UncurrySym0

(STraversable t, SMonoid m) => SingI (FoldMapDefaultSym0 :: TyFun (a ~> m) (t a ~> m) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Traversable

Methods

sing :: Sing FoldMapDefaultSym0

STraversable t => SingI (FmapDefaultSym0 :: TyFun (a ~> b) (t a ~> t b) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Traversable

Methods

sing :: Sing FmapDefaultSym0

SMonad m => SingI (LiftMSym0 :: TyFun (a1 ~> r) (m a1 ~> m r) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing LiftMSym0

SApplicative f => SingI (LiftASym0 :: TyFun (a ~> b) (f a ~> f b) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing LiftASym0

SFunctor f => SingI (FmapSym0 :: TyFun (a ~> b) (f a ~> f b) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing FmapSym0

SMonad m => SingI ((=<<@#@$) :: TyFun (a ~> m b) (m a ~> m b) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing (=<<@#@$)

SingI d => SingI (Maybe_Sym1 d a :: TyFun (a ~> b) (Maybe a ~> b) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Maybe

Methods

sing :: Sing (Maybe_Sym1 d a)

SingI (ListzipWithSym0 :: TyFun (a ~> (b ~> c)) ([a] ~> ([b] ~> [c])) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing ListzipWithSym0

SingI (ZipWithSym0 :: TyFun (a ~> (b ~> c)) ([a] ~> ([b] ~> [c])) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing ZipWithSym0

SingI (MapAccumRSym0 :: TyFun (acc ~> (x ~> (acc, y))) (acc ~> ([x] ~> (acc, [y]))) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing MapAccumRSym0

SingI (MapAccumLSym0 :: TyFun (acc ~> (x ~> (acc, y))) (acc ~> ([x] ~> (acc, [y]))) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing MapAccumLSym0

SFoldable t => SingI (FoldrSym0 :: TyFun (a ~> (b ~> b)) (b ~> (t a ~> b)) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing FoldrSym0

SFoldable t => SingI (Foldr'Sym0 :: TyFun (a ~> (b ~> b)) (b ~> (t a ~> b)) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing Foldr'Sym0

SFoldable t => SingI (FoldlSym0 :: TyFun (b ~> (a ~> b)) (b ~> (t a ~> b)) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing FoldlSym0

SFoldable t => SingI (Foldl'Sym0 :: TyFun (b ~> (a ~> b)) (b ~> (t a ~> b)) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing Foldl'Sym0

(SFoldable t, SMonoid m) => SingI (FoldMapSym0 :: TyFun (a ~> m) (t a ~> m) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing FoldMapSym0

SFoldable t => SingI (ConcatMapSym0 :: TyFun (a ~> [b]) (t a ~> [b]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing ConcatMapSym0

SingI (Either_Sym0 :: TyFun (a ~> c) ((b ~> c) ~> (Either a b ~> c)) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Either

Methods

sing :: Sing Either_Sym0

SingI (FlipSym0 :: TyFun (a ~> (b ~> c)) (b ~> (a ~> c)) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Base

Methods

sing :: Sing FlipSym0

SingI ((.@#@$) :: TyFun (b ~> c) ((a ~> b) ~> (a ~> c)) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Base

Methods

sing :: Sing (.@#@$)

SFunctor f => SingI ((<$>@#@$) :: TyFun (a ~> b) (f a ~> f b) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Functor

Methods

sing :: Sing (<$>@#@$)

SingI d => SingI (Option_Sym1 d a :: TyFun (a ~> b) (Option a ~> b) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Semigroup

Methods

sing :: Sing (Option_Sym1 d a)

SingI (Unzip4Sym0 :: TyFun [(a, b, c, d)] ([a], [b], [c], [d]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing Unzip4Sym0

SingI d => SingI (ListzipWithSym1 d :: TyFun [a] ([b] ~> [c]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing (ListzipWithSym1 d)

(SingI d1, SingI d2) => SingI (ListscanrSym2 d1 d2 :: TyFun [a] [b] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing (ListscanrSym2 d1 d2)

(SingI d1, SingI d2) => SingI (ListscanlSym2 d1 d2 :: TyFun [a] [b] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing (ListscanlSym2 d1 d2)

(SingI d1, SingI d2) => SingI (ListfoldrSym2 d1 d2 :: TyFun [a] b -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing (ListfoldrSym2 d1 d2)

(SingI d1, SingI d2) => SingI (ListfoldlSym2 d1 d2 :: TyFun [a] b -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing (ListfoldlSym2 d1 d2)

(SingI d1, SingI d2) => SingI (Listfoldl'Sym2 d1 d2 :: TyFun [a] b -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing (Listfoldl'Sym2 d1 d2)

SingI d => SingI (ZipWithSym1 d :: TyFun [a] ([b] ~> [c]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (ZipWithSym1 d)

SingI d => SingI (Zip3Sym1 d b c :: TyFun [b] ([c] ~> [(a, b, c)]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (Zip3Sym1 d b c)

(SingI d1, SingI d2) => SingI (ScanrSym2 d1 d2 :: TyFun [a] [b] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (ScanrSym2 d1 d2)

(SingI d1, SingI d2) => SingI (ScanlSym2 d1 d2 :: TyFun [a] [b] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (ScanlSym2 d1 d2)

(SingI d1, SingI d2) => SingI (Foldl'Sym2 d1 d2 :: TyFun [a] b -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (Foldl'Sym2 d1 d2)

(SingI d1, SingI d2) => SingI (FoldrSym2 d1 d2 :: TyFun [a] b -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Base

Methods

sing :: Sing (FoldrSym2 d1 d2)

(SingI d1, SingI d2) => SingI (FoldlSym2 d1 d2 :: TyFun [a] b -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Instances

Methods

sing :: Sing (FoldlSym2 d1 d2)

(SingI d1, SingI d2) => SingI (Maybe_Sym2 d1 d2 :: TyFun (Maybe a) b -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Maybe

Methods

sing :: Sing (Maybe_Sym2 d1 d2)

SingI d => SingI (UncurrySym1 d :: TyFun (a, b) c -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Tuple

Methods

sing :: Sing (UncurrySym1 d)

SingI d => SingI (CurrySym1 d :: TyFun a (b ~> c) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Tuple

Methods

sing :: Sing (CurrySym1 d)

(STraversable t, SApplicative f) => SingI (ForSym0 :: TyFun (t a) ((a ~> f b) ~> f (t b)) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Traversable

Methods

sing :: Sing ForSym0

(STraversable t, SMonad m) => SingI (ForMSym0 :: TyFun (t a) ((a ~> m b) ~> m (t b)) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Traversable

Methods

sing :: Sing ForMSym0

(STraversable t, SMonoid m, SingI d) => SingI (FoldMapDefaultSym1 d t :: TyFun (t a) m -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Traversable

Methods

sing :: Sing (FoldMapDefaultSym1 d t)

(STraversable t, SingI d) => SingI (FmapDefaultSym1 d t :: TyFun (t a) (t b) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Traversable

Methods

sing :: Sing (FmapDefaultSym1 d t)

(SMonadPlus m, SingI d) => SingI (MplusSym1 d :: TyFun (m a) (m a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing (MplusSym1 d)

(SMonad m, SingI d) => SingI (LiftMSym1 d m :: TyFun (m a1) (m r) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing (LiftMSym1 d m)

(SApplicative f, SingI d) => SingI (LiftASym1 d f :: TyFun (f a) (f b) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing (LiftASym1 d f)

(SFunctor f, SingI d) => SingI (FmapSym1 d f :: TyFun (f a) (f b) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing (FmapSym1 d f)

(SMonad m, SingI d) => SingI (ApSym1 d :: TyFun (m a) (m b) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing (ApSym1 d)

SMonad m => SingI ((>>@#@$) :: TyFun (m a) (m b ~> m b) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing (>>@#@$)

(SMonad m, SingI d) => SingI ((=<<@#@$$) d :: TyFun (m a) (m b) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing ((=<<@#@$$) d)

(SAlternative f, SingI d) => SingI ((<|>@#@$$) d :: TyFun (f a) (f a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing ((<|>@#@$$) d)

SApplicative f => SingI ((<*@#@$) :: TyFun (f a) (f b ~> f a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing (<*@#@$)

(SApplicative f, SingI d) => SingI ((<*>@#@$$) d :: TyFun (f a) (f b) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing ((<*>@#@$$) d)

(SApplicative f, SingI d) => SingI (d <**>@#@$$ b :: TyFun (f (a ~> b)) (f b) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing (d <**>@#@$$ b)

(SFunctor f, SingI d) => SingI ((d <$@#@$$ b) f :: TyFun (f b) (f a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing ((d <$@#@$$ b) f)

SApplicative f => SingI ((*>@#@$) :: TyFun (f a) (f b ~> f b) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing (*>@#@$)

SingI d => SingI (MapAccumRSym1 d :: TyFun acc ([x] ~> (acc, [y])) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (MapAccumRSym1 d)

SingI d => SingI (MapAccumLSym1 d :: TyFun acc ([x] ~> (acc, [y])) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (MapAccumLSym1 d)

(SFoldable t, SMonadPlus m) => SingI (MsumSym0 :: TyFun (t (m a)) (m a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing MsumSym0

(SFoldable t, SApplicative f) => SingI (For_Sym0 :: TyFun (t a) ((a ~> f b) ~> f ()) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing For_Sym0

(SFoldable t, SMonad m) => SingI (ForM_Sym0 :: TyFun (t a) ((a ~> m b) ~> m ()) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing ForM_Sym0

(SFoldable t, SingI d) => SingI (FoldrSym1 d t :: TyFun b (t a ~> b) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing (FoldrSym1 d t)

(SFoldable t, SingI d) => SingI (Foldr'Sym1 d t :: TyFun b (t a ~> b) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing (Foldr'Sym1 d t)

(SFoldable t, SingI d) => SingI (FoldlSym1 d t :: TyFun b (t a ~> b) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing (FoldlSym1 d t)

(SFoldable t, SingI d) => SingI (Foldl'Sym1 d t :: TyFun b (t a ~> b) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing (Foldl'Sym1 d t)

(SFoldable t, SMonoid m, SingI d) => SingI (FoldMapSym1 d t :: TyFun (t a) m -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing (FoldMapSym1 d t)

(SFoldable t, SingI d) => SingI (ConcatMapSym1 d t :: TyFun (t a) [b] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing (ConcatMapSym1 d t)

(SFoldable t, SAlternative f) => SingI (AsumSym0 :: TyFun (t (f a)) (f a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing AsumSym0

SingI d => SingI (FlipSym1 d :: TyFun b (a ~> c) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Base

Methods

sing :: Sing (FlipSym1 d)

SingI (Tuple4Sym0 :: TyFun a (b ~> (c ~> (d ~> (a, b, c, d)))) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Instances

Methods

sing :: Sing Tuple4Sym0

SingI d => SingI (Tuple3Sym1 d b c :: TyFun b (c ~> (a, b, c)) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Instances

Methods

sing :: Sing (Tuple3Sym1 d b c)

(SOrd a, SingI d1, SingI d2) => SingI (ComparingSym2 d1 d2 :: TyFun b Ordering -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Ord

Methods

sing :: Sing (ComparingSym2 d1 d2)

(SFunctor f, SingI d) => SingI (d <$>@#@$$ f :: TyFun (f a) (f b) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Functor

Methods

sing :: Sing (d <$>@#@$$ f)

(SFunctor f, SingI d) => SingI (d $>@#@$$ b :: TyFun b (f b) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Functor

Methods

sing :: Sing (d $>@#@$$ b)

(SingI d1, SingI d2) => SingI (Option_Sym2 d1 d2 :: TyFun (Option a) b -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Semigroup

Methods

sing :: Sing (Option_Sym2 d1 d2)

(STraversable t, SApplicative f) => SingI (TraverseSym0 :: TyFun (a ~> f b) (t a ~> f (t b)) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Traversable

Methods

sing :: Sing TraverseSym0

(STraversable t, SMonad m) => SingI (MapMSym0 :: TyFun (a ~> m b) (t a ~> m (t b)) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Traversable

Methods

sing :: Sing MapMSym0

STraversable t => SingI (MapAccumRSym0 :: TyFun (a ~> (b ~> (a, c))) (a ~> (t b ~> (a, t c))) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Traversable

Methods

sing :: Sing MapAccumRSym0

STraversable t => SingI (MapAccumLSym0 :: TyFun (a ~> (b ~> (a, c))) (a ~> (t b ~> (a, t c))) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Traversable

Methods

sing :: Sing MapAccumLSym0

SMonad m => SingI (LiftM2Sym0 :: TyFun (a1 ~> (a2 ~> r)) (m a1 ~> (m a2 ~> m r)) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing LiftM2Sym0

SApplicative f => SingI (LiftA2Sym0 :: TyFun (a ~> (b ~> c)) (f a ~> (f b ~> f c)) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing LiftA2Sym0

(SMonad m, SingI d) => SingI (d >>=@#@$$ b :: TyFun (a ~> m b) (m b) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing (d >>=@#@$$ b)

SingI (ZipWith3Sym0 :: TyFun (a ~> (b ~> (c ~> d))) ([a] ~> ([b] ~> ([c] ~> [d]))) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing ZipWith3Sym0

(SFoldable t, SApplicative f) => SingI (Traverse_Sym0 :: TyFun (a ~> f b) (t a ~> f ()) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing Traverse_Sym0

(SFoldable t, SMonad m) => SingI (MapM_Sym0 :: TyFun (a ~> m b) (t a ~> m ()) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing MapM_Sym0

(SFoldable t, SMonad m) => SingI (FoldrMSym0 :: TyFun (a ~> (b ~> m b)) (b ~> (t a ~> m b)) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing FoldrMSym0

(SFoldable t, SMonad m) => SingI (FoldlMSym0 :: TyFun (b ~> (a ~> m b)) (b ~> (t a ~> m b)) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing FoldlMSym0

SingI d => SingI (Either_Sym1 d b :: TyFun (b ~> c) (Either a b ~> c) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Either

Methods

sing :: Sing (Either_Sym1 d b)

SingI d => SingI (d .@#@$$ a :: TyFun (a ~> b) (a ~> c) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Base

Methods

sing :: Sing (d .@#@$$ a)

(SFunctor f, SingI d) => SingI (d <&>@#@$$ b :: TyFun (a ~> b) (f b) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Functor

Methods

sing :: Sing (d <&>@#@$$ b)

SingI k2 => SingI (k2 :-> v2 :: Mapping k1 v1) Source # 
Instance details

Defined in Data.NamedSOP.Type

Methods

sing :: Sing (k2 :-> v2)

SingI (Unzip5Sym0 :: TyFun [(a, b, c, d, e)] ([a], [b], [c], [d], [e]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing Unzip5Sym0

(SingI d1, SingI d2) => SingI (ListzipWithSym2 d1 d2 :: TyFun [b] [c] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing (ListzipWithSym2 d1 d2)

(SingI d1, SingI d2) => SingI (ZipWithSym2 d1 d2 :: TyFun [b] [c] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (ZipWithSym2 d1 d2)

SingI d2 => SingI (ZipWith3Sym1 d2 :: TyFun [a] ([b] ~> ([c] ~> [d1])) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (ZipWith3Sym1 d2)

(SingI d1, SingI d2) => SingI (Zip3Sym2 d1 d2 c :: TyFun [c] [(a, b, c)] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (Zip3Sym2 d1 d2 c)

(SingI d1, SingI d2) => SingI (MapAccumRSym2 d1 d2 :: TyFun [x] (acc, [y]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (MapAccumRSym2 d1 d2)

(SingI d1, SingI d2) => SingI (MapAccumLSym2 d1 d2 :: TyFun [x] (acc, [y]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (MapAccumLSym2 d1 d2)

(SingI d1, SingI d2) => SingI (Either_Sym2 d1 d2 :: TyFun (Either a b) c -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Either

Methods

sing :: Sing (Either_Sym2 d1 d2)

(SingI d1, SingI d2) => SingI (CurrySym2 d1 d2 :: TyFun b c -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Tuple

Methods

sing :: Sing (CurrySym2 d1 d2)

(STraversable t, SApplicative f, SingI d) => SingI (TraverseSym1 d t :: TyFun (t a) (f (t b)) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Traversable

Methods

sing :: Sing (TraverseSym1 d t)

(STraversable t, SMonad m, SingI d) => SingI (MapMSym1 d t :: TyFun (t a) (m (t b)) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Traversable

Methods

sing :: Sing (MapMSym1 d t)

(STraversable t, SingI d) => SingI (MapAccumRSym1 d t :: TyFun a (t b ~> (a, t c)) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Traversable

Methods

sing :: Sing (MapAccumRSym1 d t)

(STraversable t, SingI d) => SingI (MapAccumLSym1 d t :: TyFun a (t b ~> (a, t c)) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Traversable

Methods

sing :: Sing (MapAccumLSym1 d t)

(SMonad m, SingI d) => SingI (LiftM2Sym1 d m :: TyFun (m a1) (m a2 ~> m r) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing (LiftM2Sym1 d m)

(SApplicative f, SingI d) => SingI (LiftA2Sym1 d f :: TyFun (f a) (f b ~> f c) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing (LiftA2Sym1 d f)

(SMonad m, SingI d) => SingI (d >>@#@$$ b :: TyFun (m b) (m b) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing (d >>@#@$$ b)

(SApplicative f, SingI d) => SingI (d <*@#@$$ b :: TyFun (f b) (f a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing (d <*@#@$$ b)

(SApplicative f, SingI d) => SingI (d *>@#@$$ b :: TyFun (f b) (f b) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing (d *>@#@$$ b)

(SFoldable t, SApplicative f, SingI d) => SingI (Traverse_Sym1 d t :: TyFun (t a) (f ()) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing (Traverse_Sym1 d t)

(SFoldable t, SMonad m, SingI d) => SingI (MapM_Sym1 d t :: TyFun (t a) (m ()) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing (MapM_Sym1 d t)

(SFoldable t, SingI d1, SingI d2) => SingI (FoldrSym2 d1 d2 t :: TyFun (t a) b -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing (FoldrSym2 d1 d2 t)

(SFoldable t, SMonad m, SingI d) => SingI (FoldrMSym1 d t :: TyFun b (t a ~> m b) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing (FoldrMSym1 d t)

(SFoldable t, SingI d1, SingI d2) => SingI (Foldr'Sym2 d1 d2 t :: TyFun (t a) b -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing (Foldr'Sym2 d1 d2 t)

(SFoldable t, SingI d1, SingI d2) => SingI (FoldlSym2 d1 d2 t :: TyFun (t a) b -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing (FoldlSym2 d1 d2 t)

(SFoldable t, SMonad m, SingI d) => SingI (FoldlMSym1 d t :: TyFun b (t a ~> m b) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing (FoldlMSym1 d t)

(SFoldable t, SingI d1, SingI d2) => SingI (Foldl'Sym2 d1 d2 t :: TyFun (t a) b -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing (Foldl'Sym2 d1 d2 t)

(SingI d1, SingI d2) => SingI (FlipSym2 d1 d2 :: TyFun a c -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Base

Methods

sing :: Sing (FlipSym2 d1 d2)

(SingI d1, SingI d2) => SingI (d1 .@#@$$$ d2 :: TyFun a c -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Base

Methods

sing :: Sing (d1 .@#@$$$ d2)

SingI (Tuple5Sym0 :: TyFun a (b ~> (c ~> (d ~> (e ~> (a, b, c, d, e))))) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Instances

Methods

sing :: Sing Tuple5Sym0

SingI d2 => SingI (Tuple4Sym1 d2 b c d1 :: TyFun b (c ~> (d1 ~> (a, b, c, d1))) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Instances

Methods

sing :: Sing (Tuple4Sym1 d2 b c d1)

(SingI d1, SingI d2) => SingI (Tuple3Sym2 d1 d2 c :: TyFun c (a, b, c) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Instances

Methods

sing :: Sing (Tuple3Sym2 d1 d2 c)

(STraversable t, SApplicative f, SingI d) => SingI (ForSym1 d b f :: TyFun (a ~> f b) (f (t b)) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Traversable

Methods

sing :: Sing (ForSym1 d b f)

(STraversable t, SMonad m, SingI d) => SingI (ForMSym1 d b m :: TyFun (a ~> m b) (m (t b)) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Traversable

Methods

sing :: Sing (ForMSym1 d b m)

SMonad m => SingI (LiftM3Sym0 :: TyFun (a1 ~> (a2 ~> (a3 ~> r))) (m a1 ~> (m a2 ~> (m a3 ~> m r))) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing LiftM3Sym0

SApplicative f => SingI (LiftA3Sym0 :: TyFun (a ~> (b ~> (c ~> d))) (f a ~> (f b ~> (f c ~> f d))) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing LiftA3Sym0

(SFoldable t, SApplicative f, SingI d) => SingI (For_Sym1 d b f :: TyFun (a ~> f b) (f ()) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing (For_Sym1 d b f)

(SFoldable t, SMonad m, SingI d) => SingI (ForM_Sym1 d b m :: TyFun (a ~> m b) (m ()) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing (ForM_Sym1 d b m)

SingI (Unzip6Sym0 :: TyFun [(a, b, c, d, e, f)] ([a], [b], [c], [d], [e], [f]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing Unzip6Sym0

(SingI d2, SingI d3) => SingI (ZipWith3Sym2 d2 d3 :: TyFun [b] ([c] ~> [d1]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (ZipWith3Sym2 d2 d3)

(STraversable t, SingI d1, SingI d2) => SingI (MapAccumRSym2 d1 d2 t :: TyFun (t b) (a, t c) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Traversable

Methods

sing :: Sing (MapAccumRSym2 d1 d2 t)

(STraversable t, SingI d1, SingI d2) => SingI (MapAccumLSym2 d1 d2 t :: TyFun (t b) (a, t c) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Traversable

Methods

sing :: Sing (MapAccumLSym2 d1 d2 t)

(SMonad m, SingI d) => SingI (LiftM3Sym1 d m :: TyFun (m a1) (m a2 ~> (m a3 ~> m r)) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing (LiftM3Sym1 d m)

(SMonad m, SingI d1, SingI d2) => SingI (LiftM2Sym2 d1 d2 :: TyFun (m a2) (m r) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing (LiftM2Sym2 d1 d2)

(SApplicative f, SingI d2) => SingI (LiftA3Sym1 d2 f :: TyFun (f a) (f b ~> (f c ~> f d1)) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing (LiftA3Sym1 d2 f)

(SApplicative f, SingI d1, SingI d2) => SingI (LiftA2Sym2 d1 d2 :: TyFun (f b) (f c) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing (LiftA2Sym2 d1 d2)

(SFoldable t, SMonad m, SingI d1, SingI d2) => SingI (FoldrMSym2 d1 d2 t :: TyFun (t a) (m b) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing (FoldrMSym2 d1 d2 t)

(SFoldable t, SMonad m, SingI d1, SingI d2) => SingI (FoldlMSym2 d1 d2 t :: TyFun (t a) (m b) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing (FoldlMSym2 d1 d2 t)

SingI (Tuple6Sym0 :: TyFun a (b ~> (c ~> (d ~> (e ~> (f ~> (a, b, c, d, e, f)))))) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Instances

Methods

sing :: Sing Tuple6Sym0

SingI d2 => SingI (Tuple5Sym1 d2 b c d1 e :: TyFun b (c ~> (d1 ~> (e ~> (a, b, c, d1, e)))) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Instances

Methods

sing :: Sing (Tuple5Sym1 d2 b c d1 e)

(SingI d2, SingI d3) => SingI (Tuple4Sym2 d2 d3 c d1 :: TyFun c (d1 ~> (a, b, c, d1)) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Instances

Methods

sing :: Sing (Tuple4Sym2 d2 d3 c d1)

SMonad m => SingI (LiftM4Sym0 :: TyFun (a1 ~> (a2 ~> (a3 ~> (a4 ~> r)))) (m a1 ~> (m a2 ~> (m a3 ~> (m a4 ~> m r)))) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing LiftM4Sym0

SingI (Unzip7Sym0 :: TyFun [(a, b, c, d, e, f, g)] ([a], [b], [c], [d], [e], [f], [g]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing Unzip7Sym0

(SingI d2, SingI d3, SingI d4) => SingI (ZipWith3Sym3 d2 d3 d4 :: TyFun [c] [d1] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (ZipWith3Sym3 d2 d3 d4)

(SMonad m, SingI d) => SingI (LiftM4Sym1 d m :: TyFun (m a1) (m a2 ~> (m a3 ~> (m a4 ~> m r))) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing (LiftM4Sym1 d m)

(SMonad m, SingI d1, SingI d2) => SingI (LiftM3Sym2 d1 d2 :: TyFun (m a2) (m a3 ~> m r) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing (LiftM3Sym2 d1 d2)

(SApplicative f, SingI d2, SingI d3) => SingI (LiftA3Sym2 d2 d3 :: TyFun (f b) (f c ~> f d1) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing (LiftA3Sym2 d2 d3)

SingI (Tuple7Sym0 :: TyFun a (b ~> (c ~> (d ~> (e ~> (f ~> (g ~> (a, b, c, d, e, f, g))))))) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Instances

Methods

sing :: Sing Tuple7Sym0

SingI d2 => SingI (Tuple6Sym1 d2 b c d1 e f :: TyFun b (c ~> (d1 ~> (e ~> (f ~> (a, b, c, d1, e, f))))) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Instances

Methods

sing :: Sing (Tuple6Sym1 d2 b c d1 e f)

(SingI d2, SingI d3) => SingI (Tuple5Sym2 d2 d3 c d1 e :: TyFun c (d1 ~> (e ~> (a, b, c, d1, e))) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Instances

Methods

sing :: Sing (Tuple5Sym2 d2 d3 c d1 e)

(SingI d2, SingI d3, SingI d4) => SingI (Tuple4Sym3 d2 d3 d4 d1 :: TyFun d1 (a, b, c, d1) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Instances

Methods

sing :: Sing (Tuple4Sym3 d2 d3 d4 d1)

SMonad m => SingI (LiftM5Sym0 :: TyFun (a1 ~> (a2 ~> (a3 ~> (a4 ~> (a5 ~> r))))) (m a1 ~> (m a2 ~> (m a3 ~> (m a4 ~> (m a5 ~> m r))))) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing LiftM5Sym0

(SMonad m, SingI d) => SingI (LiftM5Sym1 d m :: TyFun (m a1) (m a2 ~> (m a3 ~> (m a4 ~> (m a5 ~> m r)))) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing (LiftM5Sym1 d m)

(SMonad m, SingI d1, SingI d2) => SingI (LiftM4Sym2 d1 d2 :: TyFun (m a2) (m a3 ~> (m a4 ~> m r)) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing (LiftM4Sym2 d1 d2)

(SMonad m, SingI d1, SingI d2, SingI d3) => SingI (LiftM3Sym3 d1 d2 d3 :: TyFun (m a3) (m r) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing (LiftM3Sym3 d1 d2 d3)

(SApplicative f, SingI d2, SingI d3, SingI d4) => SingI (LiftA3Sym3 d2 d3 d4 :: TyFun (f c) (f d1) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing (LiftA3Sym3 d2 d3 d4)

SingI d2 => SingI (Tuple7Sym1 d2 b c d1 e f g :: TyFun b (c ~> (d1 ~> (e ~> (f ~> (g ~> (a, b, c, d1, e, f, g)))))) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Instances

Methods

sing :: Sing (Tuple7Sym1 d2 b c d1 e f g)

(SingI d2, SingI d3) => SingI (Tuple6Sym2 d2 d3 c d1 e f :: TyFun c (d1 ~> (e ~> (f ~> (a, b, c, d1, e, f)))) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Instances

Methods

sing :: Sing (Tuple6Sym2 d2 d3 c d1 e f)

(SingI d2, SingI d3, SingI d4) => SingI (Tuple5Sym3 d2 d3 d4 d1 e :: TyFun d1 (e ~> (a, b, c, d1, e)) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Instances

Methods

sing :: Sing (Tuple5Sym3 d2 d3 d4 d1 e)

(SMonad m, SingI d1, SingI d2) => SingI (LiftM5Sym2 d1 d2 :: TyFun (m a2) (m a3 ~> (m a4 ~> (m a5 ~> m r))) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing (LiftM5Sym2 d1 d2)

(SMonad m, SingI d1, SingI d2, SingI d3) => SingI (LiftM4Sym3 d1 d2 d3 :: TyFun (m a3) (m a4 ~> m r) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing (LiftM4Sym3 d1 d2 d3)

(SingI d2, SingI d3) => SingI (Tuple7Sym2 d2 d3 c d1 e f g :: TyFun c (d1 ~> (e ~> (f ~> (g ~> (a, b, c, d1, e, f, g))))) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Instances

Methods

sing :: Sing (Tuple7Sym2 d2 d3 c d1 e f g)

(SingI d2, SingI d3, SingI d4) => SingI (Tuple6Sym3 d2 d3 d4 d1 e f :: TyFun d1 (e ~> (f ~> (a, b, c, d1, e, f))) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Instances

Methods

sing :: Sing (Tuple6Sym3 d2 d3 d4 d1 e f)

(SingI d2, SingI d3, SingI d4, SingI d5) => SingI (Tuple5Sym4 d2 d3 d4 d5 e :: TyFun e (a, b, c, d1, e) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Instances

Methods

sing :: Sing (Tuple5Sym4 d2 d3 d4 d5 e)

(SMonad m, SingI d1, SingI d2, SingI d3) => SingI (LiftM5Sym3 d1 d2 d3 :: TyFun (m a3) (m a4 ~> (m a5 ~> m r)) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing (LiftM5Sym3 d1 d2 d3)

(SMonad m, SingI d1, SingI d2, SingI d3, SingI d4) => SingI (LiftM4Sym4 d1 d2 d3 d4 :: TyFun (m a4) (m r) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing (LiftM4Sym4 d1 d2 d3 d4)

(SingI d2, SingI d3, SingI d4) => SingI (Tuple7Sym3 d2 d3 d4 d1 e f g :: TyFun d1 (e ~> (f ~> (g ~> (a, b, c, d1, e, f, g)))) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Instances

Methods

sing :: Sing (Tuple7Sym3 d2 d3 d4 d1 e f g)

(SingI d2, SingI d3, SingI d4, SingI d5) => SingI (Tuple6Sym4 d2 d3 d4 d5 e f :: TyFun e (f ~> (a, b, c, d1, e, f)) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Instances

Methods

sing :: Sing (Tuple6Sym4 d2 d3 d4 d5 e f)

(SMonad m, SingI d1, SingI d2, SingI d3, SingI d4) => SingI (LiftM5Sym4 d1 d2 d3 d4 :: TyFun (m a4) (m a5 ~> m r) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing (LiftM5Sym4 d1 d2 d3 d4)

(SingI d2, SingI d3, SingI d4, SingI d5) => SingI (Tuple7Sym4 d2 d3 d4 d5 e f g :: TyFun e (f ~> (g ~> (a, b, c, d1, e, f, g))) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Instances

Methods

sing :: Sing (Tuple7Sym4 d2 d3 d4 d5 e f g)

(SingI d2, SingI d3, SingI d4, SingI d5, SingI d6) => SingI (Tuple6Sym5 d2 d3 d4 d5 d6 f :: TyFun f (a, b, c, d1, e, f) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Instances

Methods

sing :: Sing (Tuple6Sym5 d2 d3 d4 d5 d6 f)

(SMonad m, SingI d1, SingI d2, SingI d3, SingI d4, SingI d5) => SingI (LiftM5Sym5 d1 d2 d3 d4 d5 :: TyFun (m a5) (m r) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing (LiftM5Sym5 d1 d2 d3 d4 d5)

(SingI d2, SingI d3, SingI d4, SingI d5, SingI d6) => SingI (Tuple7Sym5 d2 d3 d4 d5 d6 f g :: TyFun f (g ~> (a, b, c, d1, e, f, g)) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Instances

Methods

sing :: Sing (Tuple7Sym5 d2 d3 d4 d5 d6 f g)

(SingI d2, SingI d3, SingI d4, SingI d5, SingI d6, SingI d7) => SingI (Tuple7Sym6 d2 d3 d4 d5 d6 d7 g :: TyFun g (a, b, c, d1, e, f, g) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Instances

Methods

sing :: Sing (Tuple7Sym6 d2 d3 d4 d5 d6 d7 g)

data family Sing (a :: k) :: Type #

Instances
data Sing (a :: Bool) 
Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (a :: Bool) where
data Sing (a :: Ordering) 
Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (a :: Ordering) where
data Sing (n :: Nat) 
Instance details

Defined in Data.Singletons.TypeLits.Internal

data Sing (n :: Nat) where
data Sing (n :: Symbol) 
Instance details

Defined in Data.Singletons.TypeLits.Internal

data Sing (n :: Symbol) where
data Sing (a :: ()) 
Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (a :: ()) where
data Sing (a :: Void) 
Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (a :: Void)
data Sing (a :: All) 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (a :: All) where
data Sing (a :: Any) 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (a :: Any) where
data Sing (b :: [a]) 
Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (b :: [a]) where
  • SNil :: forall a (b :: [a]). Sing ([] :: [a])
  • SCons :: forall a (b :: [a]) (n1 :: a) (n2 :: [a]). Sing n1 -> Sing n2 -> Sing (n1 ': n2)
data Sing (b :: Maybe a) 
Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (b :: Maybe a) where
data Sing (b :: Min a) 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: Min a) where
data Sing (b :: Max a) 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: Max a) where
data Sing (b :: First a) 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: First a) where
data Sing (b :: Last a) 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: Last a) where
data Sing (a :: WrappedMonoid m) 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (a :: WrappedMonoid m) where
data Sing (b :: Option a) 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: Option a) where
data Sing (b :: Identity a) 
Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (b :: Identity a) where
data Sing (b :: First a) 
Instance details

Defined in Data.Singletons.Prelude.Monoid

data Sing (b :: First a) where
data Sing (b :: Last a) 
Instance details

Defined in Data.Singletons.Prelude.Monoid

data Sing (b :: Last a) where
data Sing (b :: Dual a) 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: Dual a) where
data Sing (b :: Sum a) 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: Sum a) where
data Sing (b :: Product a) 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: Product a) where
data Sing (b :: Down a) 
Instance details

Defined in Data.Singletons.Prelude.Ord

data Sing (b :: Down a) where
data Sing (b :: NonEmpty a) 
Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (b :: NonEmpty a) where
data Sing (b :: Endo a) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

data Sing (b :: Endo a) where
  • SEndo :: forall a (b :: Endo a) (x :: a ~> a). Sing x -> Sing (Endo x)
data Sing (b :: MinInternal a) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

data Sing (b :: MinInternal a) where
data Sing (b :: MaxInternal a) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

data Sing (b :: MaxInternal a) where
data Sing (c :: Either a b) 
Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (c :: Either a b) where
data Sing (c :: (a, b)) 
Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (c :: (a, b)) where
data Sing (c :: Arg a b) 
Instance details

Defined in Data.Singletons.Prelude.Semigroup

data Sing (c :: Arg a b) where
newtype Sing (f :: k1 ~> k2) 
Instance details

Defined in Data.Singletons.Internal

newtype Sing (f :: k1 ~> k2) = SLambda {}
data Sing (a :: Mapping k v) Source # 
Instance details

Defined in Data.NamedSOP.Type

data Sing (a :: Mapping k v) where
data Sing (b :: StateL s a) 
Instance details

Defined in Data.Singletons.Prelude.Traversable

data Sing (b :: StateL s a) where
  • SStateL :: forall s a (b :: StateL s a) (x :: s ~> (s, a)). Sing x -> Sing (StateL x)
data Sing (b :: StateR s a) 
Instance details

Defined in Data.Singletons.Prelude.Traversable

data Sing (b :: StateR s a) where
  • SStateR :: forall s a (b :: StateR s a) (x :: s ~> (s, a)). Sing x -> Sing (StateR x)
data Sing (d :: (a, b, c)) 
Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (d :: (a, b, c)) where
data Sing (c :: Const a b) 
Instance details

Defined in Data.Singletons.Prelude.Const

data Sing (c :: Const a b) where
data Sing (e :: (a, b, c, d)) 
Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (e :: (a, b, c, d)) where
data Sing (f :: (a, b, c, d, e)) 
Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (f :: (a, b, c, d, e)) where
  • STuple5 :: forall a b c d e (f :: (a, b, c, d, e)) (n1 :: a) (n2 :: b) (n3 :: c) (n4 :: d) (n5 :: e). Sing n1 -> Sing n2 -> Sing n3 -> Sing n4 -> Sing n5 -> Sing ((,,,,) n1 n2 n3 n4 n5)
data Sing (g :: (a, b, c, d, e, f)) 
Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (g :: (a, b, c, d, e, f)) where
  • STuple6 :: forall a b c d e f (g :: (a, b, c, d, e, f)) (n1 :: a) (n2 :: b) (n3 :: c) (n4 :: d) (n5 :: e) (n6 :: f). Sing n1 -> Sing n2 -> Sing n3 -> Sing n4 -> Sing n5 -> Sing n6 -> Sing ((,,,,,) n1 n2 n3 n4 n5 n6)
data Sing (h :: (a, b, c, d, e, f, g)) 
Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (h :: (a, b, c, d, e, f, g)) where
  • STuple7 :: forall a b c d e f g (h :: (a, b, c, d, e, f, g)) (n1 :: a) (n2 :: b) (n3 :: c) (n4 :: d) (n5 :: e) (n6 :: f) (n7 :: g). Sing n1 -> Sing n2 -> Sing n3 -> Sing n4 -> Sing n5 -> Sing n6 -> Sing n7 -> Sing ((,,,,,,) n1 n2 n3 n4 n5 n6 n7)