Safe Haskell	None
Language	Haskell2010

Data.NamedSOP.Type

Contents

Symbol-value mappings
List operation singletons
Convenience re-exports

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 SMapping :: forall k v (a :: Mapping k v) (k :: k) (v :: v). Sing k -> Sing (k :-> v)
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 SFalse :: forall (a :: Bool). Sing False STrue :: forall (a :: Bool). Sing True
data Sing (a :: Ordering)
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (a :: Ordering) where SLT :: forall (a :: Ordering). Sing LT SEQ :: forall (a :: Ordering). Sing EQ SGT :: forall (a :: Ordering). Sing GT
data Sing (n :: Nat)
Instance details Defined in Data.Singletons.TypeLits.Internal data Sing (n :: Nat) where SNat :: forall (n :: Nat). KnownNat n => Sing n
data Sing (n :: Symbol)
Instance details Defined in Data.Singletons.TypeLits.Internal data Sing (n :: Symbol) where SSym :: forall (n :: Symbol). KnownSymbol n => Sing n
data Sing (a :: ())
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (a :: ()) where STuple0 :: forall (a :: ()). Sing ()
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 SAll :: forall (a :: All) (n :: Bool). {..} -> Sing (All n)
data Sing (a :: Any)
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal data Sing (a :: Any) where SAny :: forall (a :: Any) (n :: Bool). {..} -> Sing (Any n)
data Sing (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 SNothing :: forall a (b :: Maybe a). Sing (Nothing :: Maybe a) SJust :: forall a (b :: Maybe a) (n :: a). Sing n -> Sing (Just n)
data Sing (b :: Min a)
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal data Sing (b :: Min a) where SMin :: forall a (b :: Min a) (n :: a). {..} -> Sing (Min n)
data Sing (b :: Max a)
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal data Sing (b :: Max a) where SMax :: forall a (b :: Max a) (n :: a). {..} -> Sing (Max n)
data Sing (b :: First a)
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal data Sing (b :: First a) where SFirst :: forall a (b :: First a) (n :: a). {..} -> Sing (First n)
data Sing (b :: Last a)
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal data Sing (b :: Last a) where SLast :: forall a (b :: Last a) (n :: a). {..} -> Sing (Last n)
data Sing (a :: WrappedMonoid m)
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal data Sing (a :: WrappedMonoid m) where SWrapMonoid :: forall m (a :: WrappedMonoid m) (n :: m). {..} -> Sing (WrapMonoid n)
data Sing (b :: Option a)
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal data Sing (b :: Option a) where SOption :: forall a (b :: Option a) (n :: Maybe a). {..} -> Sing (Option n)
data Sing (b :: Identity a)
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (b :: Identity a) where SIdentity :: forall a (b :: Identity a) (n :: a). {..} -> Sing (Identity n)
data Sing (b :: First a)
Instance details Defined in Data.Singletons.Prelude.Monoid data Sing (b :: First a) where SFirst :: forall a (b :: First a) (n :: Maybe a). {..} -> Sing (First n)
data Sing (b :: Last a)
Instance details Defined in Data.Singletons.Prelude.Monoid data Sing (b :: Last a) where SLast :: forall a (b :: Last a) (n :: Maybe a). {..} -> Sing (Last n)
data Sing (b :: Dual a)
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal data Sing (b :: Dual a) where SDual :: forall a (b :: Dual a) (n :: a). {..} -> Sing (Dual n)
data Sing (b :: Sum a)
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal data Sing (b :: Sum a) where SSum :: forall a (b :: Sum a) (n :: a). {..} -> Sing (Sum n)
data Sing (b :: Product a)
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal data Sing (b :: Product a) where SProduct :: forall a (b :: Product a) (n :: a). {..} -> Sing (Product n)
data Sing (b :: Down a)
Instance details Defined in Data.Singletons.Prelude.Ord data Sing (b :: Down a) where SDown :: forall a (b :: Down a) (n :: a). Sing n -> Sing (Down n)
data Sing (b :: NonEmpty a)
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (b :: NonEmpty a) where (:%\|) :: forall a (b :: NonEmpty a) (n1 :: a) (n2 :: [a]). Sing n1 -> Sing n2 -> Sing (n1 :\| n2)
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 SMinInternal :: forall a (b :: MinInternal a) (x :: Maybe a). Sing x -> Sing (MinInternal x)
data Sing (b :: MaxInternal a)
Instance details Defined in Data.Singletons.Prelude.Foldable data Sing (b :: MaxInternal a) where SMaxInternal :: forall a (b :: MaxInternal a) (x :: Maybe a). Sing x -> Sing (MaxInternal x)
data Sing (c :: Either a b)
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (c :: Either a b) where SLeft :: forall a b (c :: Either a b) (n :: a). Sing n -> Sing (Left n :: Either a b) SRight :: forall a b (c :: Either a b) (n :: b). Sing n -> Sing (Right n :: Either a b)
data Sing (c :: (a, b))
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (c :: (a, b)) where STuple2 :: forall a b (c :: (a, b)) (n1 :: a) (n2 :: b). Sing n1 -> Sing n2 -> Sing ((,) n1 n2)
data Sing (c :: Arg a b)
Instance details Defined in Data.Singletons.Prelude.Semigroup data Sing (c :: Arg a b) where SArg :: forall a b (c :: Arg a b) (n1 :: a) (n2 :: b). Sing n1 -> Sing n2 -> Sing (Arg n1 n2)
newtype Sing (f :: k1 ~> k2)
Instance details Defined in Data.Singletons.Internal newtype Sing (f :: k1 ~> k2) = SLambda { applySing :: forall (t :: k1). Sing t -> Sing (f @@ t) }
data Sing (a :: Mapping k v) Source #
Instance details Defined in Data.NamedSOP.Type data Sing (a :: Mapping k v) where SMapping :: forall k v (a :: Mapping k v) (k :: k) (v :: v). Sing k -> Sing (k :-> v)
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 STuple3 :: forall a b c (d :: (a, b, c)) (n1 :: a) (n2 :: b) (n3 :: c). Sing n1 -> Sing n2 -> Sing n3 -> Sing ((,,) n1 n2 n3)
data Sing (c :: Const a b)
Instance details Defined in Data.Singletons.Prelude.Const data Sing (c :: Const a b) where SConst :: forall k a (b :: k) (c :: Const a b) (a1 :: a). {..} -> Sing (Const a1 :: Const a b)
data Sing (e :: (a, b, c, d))
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (e :: (a, b, c, d)) where STuple4 :: forall a b c d (e :: (a, b, c, d)) (n1 :: a) (n2 :: b) (n3 :: c) (n4 :: d). Sing n1 -> Sing n2 -> Sing n3 -> Sing n4 -> Sing ((,,,) n1 n2 n3 n4)
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)