Data.NamedSOP.Type

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.

Symbol-value mappings

data Mapping k v

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

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

Defined in Data.NamedSOP.Sum

Methods

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

show :: NSum [] -> String

showList :: [NSum []] -> ShowS

Eq a => Eq (Mapping a b)

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)

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)

Defined in Data.NamedSOP.Type

Methods

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

show :: Mapping k v -> String

showList :: [Mapping k v] -> ShowS

POrd k => POrd (Mapping k v)

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

SOrd k => SOrd (Mapping k v)

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)

SEq k => SEq (Mapping k v)

Defined in Data.NamedSOP.Type

Methods

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

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

PEq (Mapping k v)

Equality and ordering on mappings uses only the key.

Defined in Data.NamedSOP.Type

Associated Types

type x == y :: Bool

type x /= y :: Bool

SingI k2 => SingI (k2 :-> v2 :: Mapping k1 v1)

Defined in Data.NamedSOP.Type

Methods

sing :: Sing (k2 :-> v2)

data Sing (a :: Mapping k v)

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 Min (arg :: Mapping k v) (arg1 :: Mapping k v)

Defined in Data.NamedSOP.Type

type Min (arg :: Mapping k v) (arg1 :: Mapping k v) = Apply (Apply (Min_6989586621679379693Sym0 :: TyFun (Mapping k v) (Mapping k v ~> Mapping k v) -> Type) arg) arg1

type Max (arg :: Mapping k v) (arg1 :: Mapping k v)

Defined in Data.NamedSOP.Type

type Max (arg :: Mapping k v) (arg1 :: Mapping k v) = Apply (Apply (Max_6989586621679379675Sym0 :: TyFun (Mapping k v) (Mapping k v ~> Mapping k v) -> Type) arg) arg1

type (arg :: Mapping k v) >= (arg1 :: Mapping k v)

Defined in Data.NamedSOP.Type

type (arg :: Mapping k v) >= (arg1 :: Mapping k v) = Apply (Apply (TFHelper_6989586621679379657Sym0 :: TyFun (Mapping k v) (Mapping k v ~> Bool) -> Type) arg) arg1

type (arg :: Mapping k v) > (arg1 :: Mapping k v)

Defined in Data.NamedSOP.Type

type (arg :: Mapping k v) > (arg1 :: Mapping k v) = Apply (Apply (TFHelper_6989586621679379639Sym0 :: TyFun (Mapping k v) (Mapping k v ~> Bool) -> Type) arg) arg1

type (arg :: Mapping k v) <= (arg1 :: Mapping k v)

Defined in Data.NamedSOP.Type

type (arg :: Mapping k v) <= (arg1 :: Mapping k v) = Apply (Apply (TFHelper_6989586621679379621Sym0 :: TyFun (Mapping k v) (Mapping k v ~> Bool) -> Type) arg) arg1

type (arg :: Mapping k v) < (arg1 :: Mapping k v)

Defined in Data.NamedSOP.Type

type (arg :: Mapping k v) < (arg1 :: Mapping k v) = Apply (Apply (TFHelper_6989586621679379603Sym0 :: TyFun (Mapping k v) (Mapping k v ~> Bool) -> Type) arg) arg1

type (x :: Mapping k v) /= (y :: Mapping k v)

Defined in Data.NamedSOP.Type

type (x :: Mapping k v) /= (y :: Mapping k v) = Not (x == y)

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

Defined in Data.NamedSOP.Type

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

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

Defined in Data.NamedSOP.Type

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

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

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

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

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

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

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

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

Equations

Insert x '[] = Apply (Apply (:@#@$) x) '[]

Insert x ((:) y ys) = Case_6989586621679073946 x y ys (Let6989586621679073942Scrutinee_6989586621679071307Sym3 x y ys)

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

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

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

Convenience re-exports

class SingI (a :: k)

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

Minimal complete definition

sing

Instances

SingI NotSym0

Defined in Data.Singletons.Prelude.Bool

Methods

sing :: Sing NotSym0

SingI (||@#@$)

Defined in Data.Singletons.Prelude.Bool

Methods

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

SingI (&&@#@$)

Defined in Data.Singletons.Prelude.Bool

Methods

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

SingI Log2Sym0

Defined in Data.Singletons.TypeLits

Methods

sing :: Sing Log2Sym0

SingI (<=?@#@$)

Defined in Data.Singletons.TypeLits.Internal

Methods

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

SingI ModSym0

Defined in Data.Singletons.TypeLits

Methods

sing :: Sing ModSym0

SingI DivSym0

Defined in Data.Singletons.TypeLits

Methods

sing :: Sing DivSym0

SingI (^@#@$)

Defined in Data.Singletons.TypeLits.Internal

Methods

sing :: Sing (^@#@$)

SingI AllSym0

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

sing :: Sing AllSym0

SingI AnySym0

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

sing :: Sing AnySym0

SingI ShowParenSym0

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing ShowParenSym0

SingI OrSym0

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing OrSym0

SingI AndSym0

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing AndSym0

SingI UnwordsSym0

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing UnwordsSym0

SingI UnlinesSym0

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing UnlinesSym0

SingI Show_tupleSym0

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing Show_tupleSym0

SingI ThenCmpSym0

Defined in Data.Singletons.Prelude.Ord

Methods

sing :: Sing ThenCmpSym0

SingI EftNatSym0

Defined in Data.Singletons.Prelude.Enum

Methods

sing :: Sing EftNatSym0

SingI EfdtNatDnSym0

Defined in Data.Singletons.Prelude.Enum

Methods

sing :: Sing EfdtNatDnSym0

SingI EfdtNatSym0

Defined in Data.Singletons.Prelude.Enum

Methods

sing :: Sing EfdtNatSym0

SingI EfdtNatUpSym0

Defined in Data.Singletons.Prelude.Enum

Methods

sing :: Sing EfdtNatUpSym0

SingI ShowSpaceSym0

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing ShowSpaceSym0

SingI ShowCommaSpaceSym0

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing ShowCommaSpaceSym0

SingI ShowStringSym0

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing ShowStringSym0

SingI ShowCharSym0

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing ShowCharSym0

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

Defined in Data.Singletons.Prelude.Bool

Methods

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

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

Defined in Data.Singletons.Prelude.Bool

Methods

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

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

Defined in Data.Singletons.TypeLits.Internal

Methods

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

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

Defined in Data.Singletons.TypeLits

Methods

sing :: Sing (ModSym1 x)

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

Defined in Data.Singletons.TypeLits

Methods

sing :: Sing (DivSym1 x)

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

Defined in Data.Singletons.TypeLits.Internal

Methods

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

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

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing GuardSym0

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

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing WhenSym0

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

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

Methods

sing :: Sing ListtransposeSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing TransposeSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing ConcatSym0

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

Defined in Data.Singletons.Prelude.Maybe

Methods

sing :: Sing CatMaybesSym0

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

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing ShowListSym0

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

Defined in Data.Singletons.Prelude.Maybe

Methods

sing :: Sing ListToMaybeSym0

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

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

Methods

sing :: Sing ListtailsSym0

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

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

Methods

sing :: Sing ListsumSym0

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

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

Methods

sing :: Sing ListsortSym0

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

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

Methods

sing :: Sing ListreverseSym0

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

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

Methods

sing :: Sing ListproductSym0

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

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

Methods

sing :: Sing ListnullSym0

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

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

Methods

sing :: Sing ListminimumSym0

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

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

Methods

sing :: Sing ListmaximumSym0

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

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

Methods

sing :: Sing ListlengthSym0

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

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

Methods

sing :: Sing ListlastSym0

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

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

Methods

sing :: Sing ListisPrefixOfSym0

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

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

Methods

sing :: Sing ListinitsSym0

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

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

Methods

sing :: Sing ListinitSym0

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

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

Methods

sing :: Sing ListindexSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

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

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing UnionSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing TailsSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing TailSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing SumSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing SubsequencesSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing SortSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing ReverseSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing ProductSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing PermutationsSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing NullSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing NubSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing NonEmptySubsequencesSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing MinimumSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing MaximumSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing LengthSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing LastSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing IsSuffixOfSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing IsPrefixOfSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing IsInfixOfSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing IntersectSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing IntercalateSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing InitsSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing InitSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing HeadSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing GroupSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

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

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

Defined in Data.Singletons.Prelude.Base

Methods

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

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

Defined in Data.Singletons.Prelude.Monoid

Methods

sing :: Sing MconcatSym0

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

Defined in Data.Singletons.Prelude.Maybe

Methods

sing :: Sing MaybeToListSym0

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

Defined in Data.Singletons.Prelude.Maybe

Methods

sing :: Sing IsNothingSym0

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

Defined in Data.Singletons.Prelude.Maybe

Methods

sing :: Sing IsJustSym0

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

Defined in Data.Singletons.Prelude.Maybe

Methods

sing :: Sing FromJustSym0

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

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

sing :: Sing OptionSym0

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

Defined in Data.Singletons.Prelude.Monoid

Methods

sing :: Sing LastSym0

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

Defined in Data.Singletons.Prelude.Monoid

Methods

sing :: Sing FirstSym0

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

Defined in Data.Singletons.Prelude.Ord

Methods

sing :: Sing (ThenCmpSym1 d)

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

Defined in Data.Singletons.Prelude.Enum

Methods

sing :: Sing (EftNatSym1 d)

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

Defined in Data.Singletons.Prelude.Num

Methods

sing :: Sing FromIntegerSym0

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

Defined in Data.Singletons.Prelude.Enum

Methods

sing :: Sing ToEnumSym0

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

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

Methods

sing :: Sing ListtakeSym0

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

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

Methods

sing :: Sing ListsplitAtSym0

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

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

Methods

sing :: Sing ListdropSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing TakeSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing SplitAtSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing DropSym0

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

Defined in Data.Singletons.Prelude.Enum

Methods

sing :: Sing (EfdtNatDnSym1 d)

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

Defined in Data.Singletons.Prelude.Enum

Methods

sing :: Sing (EfdtNatSym1 d)

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

Defined in Data.Singletons.Prelude.Enum

Methods

sing :: Sing (EfdtNatUpSym1 d)

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

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing ShowsPrecSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing ReplicateSym0

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

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing (ShowStringSym1 d)

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

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing (ShowCharSym1 d)

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

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing (Show_tupleSym1 d)

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

Defined in Data.Singletons.Prelude.IsString

Methods

sing :: Sing FromStringSym0

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

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing ShowsSym0

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

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing Show_Sym0

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

Defined in Data.Singletons.Prelude.Num

Methods

sing :: Sing SubtractSym0

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

Defined in Data.Singletons.Prelude.Num

Methods

sing :: Sing SignumSym0

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

Defined in Data.Singletons.Prelude.Num

Methods

sing :: Sing NegateSym0

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

Defined in Data.Singletons.Prelude.Num

Methods

sing :: Sing AbsSym0

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

Defined in Data.Singletons.Prelude.Num

Methods

sing :: Sing (-@#@$)

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

Defined in Data.Singletons.Prelude.Num

Methods

sing :: Sing (+@#@$)

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

Defined in Data.Singletons.Prelude.Num

Methods

sing :: Sing (*@#@$)

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

Defined in Data.Singletons.Prelude.Maybe

Methods

sing :: Sing FromMaybeSym0

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

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

Methods

sing :: Sing ListintersperseSym0

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

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

Methods

sing :: Sing ListinsertSym0

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

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

Methods

sing :: Sing ListelemSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing PrependToAllSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing NotElemSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing IntersperseSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing InsertSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing ElemSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing ElemIndicesSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing ElemIndexSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing DeleteSym0

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

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing OrSym0

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

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing AndSym0

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

Defined in Data.Singletons.Prelude.Enum

Methods

sing :: Sing SuccSym0

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

Defined in Data.Singletons.Prelude.Enum

Methods

sing :: Sing PredSym0

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

Defined in Data.Singletons.Prelude.Enum

Methods

sing :: Sing FromEnumSym0

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

Defined in Data.Singletons.Prelude.Enum

Methods

sing :: Sing EnumFromToSym0

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

Defined in Data.Singletons.Prelude.Enum

Methods

sing :: Sing EnumFromThenToSym0

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

Defined in Data.Singletons.Prelude.Bool

Methods

sing :: Sing Bool_Sym0

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

Defined in Data.Singletons.Prelude.Base

Methods

sing :: Sing IdSym0

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

Defined in Data.Singletons.Prelude.Base

Methods

sing :: Sing AsTypeOfSym0

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

Defined in Data.Singletons.Prelude.Eq

Methods

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

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

Defined in Data.Singletons.Prelude.Eq

Methods

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

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

Defined in Data.Singletons.Prelude.Instances

Methods

sing :: Sing JustSym0

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

Defined in Data.Singletons.Prelude.Instances

Methods

sing :: Sing IdentitySym0

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

Defined in Data.Singletons.Prelude.Instances

Methods

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

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

Defined in Data.Singletons.Prelude.Instances

Methods

sing :: Sing (:@#@$)

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

Defined in Data.Singletons.Prelude.Ord

Methods

sing :: Sing MinSym0

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

Defined in Data.Singletons.Prelude.Ord

Methods

sing :: Sing MaxSym0

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

Defined in Data.Singletons.Prelude.Ord

Methods

sing :: Sing DownSym0

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

Defined in Data.Singletons.Prelude.Ord

Methods

sing :: Sing CompareSym0

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

Defined in Data.Singletons.Prelude.Ord

Methods

sing :: Sing (>@#@$)

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

Defined in Data.Singletons.Prelude.Ord

Methods

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

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

Defined in Data.Singletons.Prelude.Ord

Methods

sing :: Sing (<@#@$)

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

Defined in Data.Singletons.Prelude.Ord

Methods

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

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

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

sing :: Sing WrapMonoidSym0

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

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

sing :: Sing SumSym0

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

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

sing :: Sing ProductSym0

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

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

sing :: Sing MinSym0

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

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

sing :: Sing MaxSym0

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

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

sing :: Sing LastSym0

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

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

sing :: Sing FirstSym0

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

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

sing :: Sing DualSym0

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

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

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

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

Defined in Data.Singletons.Prelude.Monoid

Methods

sing :: Sing MappendSym0

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

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

sing :: Sing SconcatSym0

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

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing (ShowParenSym1 d)

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

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing ShowListWithSym0

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

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

Methods

sing :: Sing ListtakeWhileSym0

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

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

Methods

sing :: Sing ListspanSym0

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

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

Methods

sing :: Sing ListsortBySym0

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

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

Methods

sing :: Sing Listscanr1Sym0

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

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

Methods

sing :: Sing ListpartitionSym0

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

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

Methods

sing :: Sing ListnubBySym0

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

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

Methods

sing :: Sing Listfoldr1Sym0

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

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

Methods

sing :: Sing Listfoldl1Sym0

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

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

Methods

sing :: Sing ListfilterSym0

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

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

Methods

sing :: Sing ListdropWhileSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing UnionBySym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing TakeWhileSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing SpanSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing SortBySym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing SelectSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing Scanr1Sym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing Scanl1Sym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing PartitionSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing NubBySym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing MinimumBySym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing MaximumBySym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing IntersectBySym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing InsertBySym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing GroupBySym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing Foldr1Sym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing Foldl1Sym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing Foldl1'Sym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing FindSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing FindIndicesSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing FindIndexSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing FilterSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing Elem_bySym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing DropWhileSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing DropWhileEndSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing DeleteFirstsBySym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing DeleteBySym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing BreakSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing AnySym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing AllSym0

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

Defined in Data.Singletons.Prelude.Base

Methods

sing :: Sing UntilSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (IntercalateSym1 d)

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

Defined in Data.Singletons.Prelude.Either

Methods

sing :: Sing RightsSym0

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

Defined in Data.Singletons.Prelude.Either

Methods

sing :: Sing PartitionEithersSym0

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

Defined in Data.Singletons.Prelude.Either

Methods

sing :: Sing LeftsSym0

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

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

Methods

sing :: Sing ListunzipSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing UnzipSym0

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

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing (ShowListWithSym1 d)

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

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

Methods

sing :: Sing ListzipSym0

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

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

Methods

sing :: Sing (ListtakeWhileSym1 d)

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

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)

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

Methods

sing :: Sing (ListsplitAtSym1 d a)

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

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

Methods

sing :: Sing (ListspanSym1 d)

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

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

Methods

sing :: Sing (ListsortBySym1 d)

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

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

Methods

sing :: Sing (Listscanr1Sym1 d)

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

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

Methods

sing :: Sing (ListpartitionSym1 d)

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

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

Methods

sing :: Sing (ListnubBySym1 d)

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

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

Methods

sing :: Sing (ListisPrefixOfSym1 d)

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

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

Methods

sing :: Sing (ListintersperseSym1 d)

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

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

Methods

sing :: Sing (ListinsertSym1 d)

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

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

Methods

sing :: Sing (Listfoldr1Sym1 d)

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

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

Methods

sing :: Sing (Listfoldl1Sym1 d)

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

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

Methods

sing :: Sing (ListfilterSym1 d)

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

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

Methods

sing :: Sing (ListelemSym1 d)

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

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

Methods

sing :: Sing (ListdropWhileSym1 d)

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

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

Methods

sing :: Sing (ListdropSym1 d a)

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

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

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing ZipSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (UnionSym1 d)

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (UnionBySym1 d)

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (TakeWhileSym1 d)

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (TakeSym1 d a)

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (SplitAtSym1 d a)

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (SpanSym1 d)

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (SortBySym1 d)

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (Scanr1Sym1 d)

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (Scanl1Sym1 d)

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (PrependToAllSym1 d)

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (PartitionSym1 d)

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (NubBySym1 d)

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (NotElemSym1 d)

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (MinimumBySym1 d)

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (MaximumBySym1 d)

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (IsSuffixOfSym1 d)

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (IsPrefixOfSym1 d)

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (IsInfixOfSym1 d)

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (IntersperseSym1 d)

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (IntersectSym1 d)

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (IntersectBySym1 d)

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (InsertSym1 d)

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (GroupBySym1 d)

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing GenericLengthSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (Foldr1Sym1 d)

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (Foldl1Sym1 d)

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (Foldl1'Sym1 d)

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (FindSym1 d)

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (FindIndicesSym1 d)

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (FindIndexSym1 d)

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (FilterSym1 d)

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (ElemSym1 d)

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (ElemIndicesSym1 d)

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (ElemIndexSym1 d)

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (DropWhileSym1 d)

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (DropWhileEndSym1 d)

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (DropSym1 d a)

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (DeleteSym1 d)

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (DeleteFirstsBySym1 d)

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (BreakSym1 d)

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (AnySym1 d)

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (AllSym1 d)

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

Defined in Data.Singletons.Prelude.Base

Methods

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

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

Defined in Data.Singletons.Prelude.Instances

Methods

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

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

Defined in Data.Singletons.Prelude.Instances

Methods

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

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

Defined in Data.Singletons.Prelude.Maybe

Methods

sing :: Sing (FromMaybeSym1 d)

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

Defined in Data.Singletons.Prelude.Either

Methods

sing :: Sing IsRightSym0

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

Defined in Data.Singletons.Prelude.Either

Methods

sing :: Sing IsLeftSym0

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

Defined in Data.Singletons.Prelude.Enum

Methods

sing :: Sing (EfdtNatDnSym2 d1 d2)

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

Defined in Data.Singletons.Prelude.Enum

Methods

sing :: Sing (EfdtNatSym2 d1 d2)

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

Defined in Data.Singletons.Prelude.Enum

Methods

sing :: Sing (EfdtNatUpSym2 d1 d2)

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

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

Methods

sing :: Sing (ListindexSym1 d)

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

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

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

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing (ShowParenSym2 d1 d2)

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

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing (ShowsSym1 d)

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

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing (ShowListSym1 d)

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

Defined in Data.Singletons.TypeLits.Internal

Methods

sing :: Sing ErrorWithoutStackTraceSym0

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

Defined in Data.Singletons.TypeLits.Internal

Methods

sing :: Sing ErrorSym0

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

Defined in Data.Singletons.Prelude.Tuple

Methods

sing :: Sing SwapSym0

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

Defined in Data.Singletons.Prelude.Tuple

Methods

sing :: Sing SndSym0

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

Defined in Data.Singletons.Prelude.Tuple

Methods

sing :: Sing FstSym0

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

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing (ShowsPrecSym1 d a)

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

Defined in Data.Singletons.Prelude.Num

Methods

sing :: Sing (SubtractSym1 d)

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

Defined in Data.Singletons.Prelude.Num

Methods

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

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

Defined in Data.Singletons.Prelude.Num

Methods

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

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

Defined in Data.Singletons.Prelude.Num

Methods

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

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

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing (WhenSym1 d f)

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

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing ReturnSym0

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

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing PureSym0

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

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing JoinSym0

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

Defined in Data.Singletons.Prelude.Maybe

Methods

sing :: Sing Maybe_Sym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (SelectSym1 d)

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (ReplicateSym1 d a)

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing LookupSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (InsertBySym1 d)

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (Elem_bySym1 d)

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (DeleteBySym1 d)

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

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing ToListSym0

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

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing SumSym0

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

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing ProductSym0

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

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing NotElemSym0

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

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing MinimumSym0

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

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing MaximumSym0

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

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing FoldSym0

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

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing ElemSym0

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

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing ConcatSym0

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

Defined in Data.Singletons.Prelude.Enum

Methods

sing :: Sing (EnumFromToSym1 d)

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

Defined in Data.Singletons.Prelude.Enum

Methods

sing :: Sing (EnumFromThenToSym1 d)

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

Defined in Data.Singletons.Prelude.Bool

Methods

sing :: Sing (Bool_Sym1 d)

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

Defined in Data.Singletons.Prelude.Base

Methods

sing :: Sing SeqSym0

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

Defined in Data.Singletons.Prelude.Base

Methods

sing :: Sing ConstSym0

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

Defined in Data.Singletons.Prelude.Base

Methods

sing :: Sing (AsTypeOfSym1 d)

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

Defined in Data.Singletons.Prelude.Eq

Methods

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

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

Defined in Data.Singletons.Prelude.Eq

Methods

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

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

Defined in Data.Singletons.Prelude.Instances

Methods

sing :: Sing Tuple2Sym0

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

Defined in Data.Singletons.Prelude.Instances

Methods

sing :: Sing RightSym0

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

Defined in Data.Singletons.Prelude.Instances

Methods

sing :: Sing LeftSym0

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

Defined in Data.Singletons.Prelude.Ord

Methods

sing :: Sing (MinSym1 d)

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

Defined in Data.Singletons.Prelude.Ord

Methods

sing :: Sing (MaxSym1 d)

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

Defined in Data.Singletons.Prelude.Ord

Methods

sing :: Sing (CompareSym1 d)

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

Defined in Data.Singletons.Prelude.Ord

Methods

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

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

Defined in Data.Singletons.Prelude.Ord

Methods

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

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

Defined in Data.Singletons.Prelude.Ord

Methods

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

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

Defined in Data.Singletons.Prelude.Ord

Methods

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

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

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

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

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

Defined in Data.Singletons.Prelude.Monoid

Methods

sing :: Sing (MappendSym1 d)

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

Defined in Data.Singletons.Prelude.Functor

Methods

sing :: Sing VoidSym0

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

Defined in Data.Singletons.Prelude.Applicative

Methods

sing :: Sing OptionalSym0

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

Defined in Data.Singletons.Prelude.Semigroup

Methods

sing :: Sing Option_Sym0

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

Defined in Data.Singletons.Prelude.Semigroup

Methods

sing :: Sing ArgSym0

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

Defined in Data.Singletons.Prelude.Maybe

Methods

sing :: Sing MapMaybeSym0

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

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

Methods

sing :: Sing ListscanrSym0

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

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

Methods

sing :: Sing ListscanlSym0

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

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

Methods

sing :: Sing ListmapSym0

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

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

Methods

sing :: Sing ListfoldrSym0

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

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

Methods

sing :: Sing ListfoldlSym0

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

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

Methods

sing :: Sing Listfoldl'Sym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing UnfoldrSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing ScanrSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing ScanlSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing Foldl'Sym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing ConcatMapSym0

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

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing MinimumBySym0

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

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing MaximumBySym0

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

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing Foldr1Sym0

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

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing Foldl1Sym0

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

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing FindSym0

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

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing AnySym0

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

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing AllSym0

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

Defined in Data.Singletons.Prelude.Base

Methods

sing :: Sing (UntilSym1 d)

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

Defined in Data.Singletons.Prelude.Base

Methods

sing :: Sing MapSym0

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

Defined in Data.Singletons.Prelude.Base

Methods

sing :: Sing FoldrSym0

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

Defined in Data.Singletons.Prelude.Base

Methods

sing :: Sing ($@#@$)

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

Defined in Data.Singletons.Prelude.Base

Methods

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

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

Defined in Data.Singletons.Prelude.Instances

Methods

sing :: Sing FoldlSym0

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

Defined in Data.Singletons.Prelude.Ord

Methods

sing :: Sing ComparingSym0

SingI (ConstSym0 :: TyFun a6989586621679077703 (Const a6989586621679077703 b6989586621679077704) -> Type)

Defined in Data.Singletons.Prelude.Const

Methods

sing :: Sing ConstSym0

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

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)

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (LookupSym1 d b)

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing Unzip3Sym0

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

Defined in Data.Singletons.Prelude.Maybe

Methods

sing :: Sing (MapMaybeSym1 d)

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

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

Methods

sing :: Sing (ListzipSym1 d b)

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

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

Methods

sing :: Sing (ListmapSym1 d)

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (ZipSym1 d b)

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing Zip3Sym0

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

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)

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)

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)

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)

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)

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (DeleteBySym2 d1 d2)

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (ConcatMapSym1 d)

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

Defined in Data.Singletons.Prelude.Base

Methods

sing :: Sing (MapSym1 d)

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

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing (ShowListWithSym2 d1 d2)

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

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing (ShowsPrecSym2 d1 d2)

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

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)

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)

Defined in Data.Singletons.Prelude.Traversable

Methods

sing :: Sing SequenceSym0

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

Defined in Data.Singletons.Prelude.Traversable

Methods

sing :: Sing SequenceASym0

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

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing MplusSym0

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

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing ApSym0

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

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

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

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

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

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

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

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

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

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

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

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

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

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

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

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

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

Methods

sing :: Sing (ListscanrSym1 d)

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

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

Methods

sing :: Sing (ListscanlSym1 d)

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

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

Methods

sing :: Sing (ListfoldrSym1 d)

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

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

Methods

sing :: Sing (ListfoldlSym1 d)

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

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

Methods

sing :: Sing (Listfoldl'Sym1 d)

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (UnfoldrSym1 d)

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (ScanrSym1 d)

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (ScanlSym1 d)

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

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)

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing Sequence_Sym0

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

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing SequenceA_Sym0

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

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)

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)

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)

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing (MaximumBySym1 d t)

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

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing LengthSym0

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

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)

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)

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)

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)

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)

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)

Defined in Data.Singletons.Prelude.Enum

Methods

sing :: Sing (EnumFromThenToSym2 d1 d2)

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

Defined in Data.Singletons.Prelude.Base

Methods

sing :: Sing (UntilSym2 d1 d2)

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

Defined in Data.Singletons.Prelude.Base

Methods

sing :: Sing (SeqSym1 d b)

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

Defined in Data.Singletons.Prelude.Base

Methods

sing :: Sing (FoldrSym1 d)

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

Defined in Data.Singletons.Prelude.Base

Methods

sing :: Sing (ConstSym1 d b)

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

Defined in Data.Singletons.Prelude.Base

Methods

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

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

Defined in Data.Singletons.Prelude.Base

Methods

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

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

Defined in Data.Singletons.Prelude.Instances

Methods

sing :: Sing Tuple3Sym0

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

Defined in Data.Singletons.Prelude.Instances

Methods

sing :: Sing (Tuple2Sym1 d b)

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

Defined in Data.Singletons.Prelude.Instances

Methods

sing :: Sing (FoldlSym1 d)

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

Defined in Data.Singletons.Prelude.Ord

Methods

sing :: Sing (ComparingSym1 d)

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

Defined in Data.Singletons.Prelude.Functor

Methods

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

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

Defined in Data.Singletons.Prelude.Functor

Methods

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

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

Defined in Data.Singletons.Prelude.Semigroup

Methods

sing :: Sing (ArgSym1 d b)

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

Defined in Data.Singletons.Prelude.Tuple

Methods

sing :: Sing CurrySym0

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

Defined in Data.Singletons.Prelude.Tuple

Methods

sing :: Sing UncurrySym0

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

Defined in Data.Singletons.Prelude.Traversable

Methods

sing :: Sing FoldMapDefaultSym0

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

Defined in Data.Singletons.Prelude.Traversable

Methods

sing :: Sing FmapDefaultSym0

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

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing LiftMSym0

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

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing LiftASym0

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

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing FmapSym0

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

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

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

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

Defined in Data.Singletons.Prelude.Maybe

Methods

sing :: Sing (Maybe_Sym1 d a)

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

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

Methods

sing :: Sing ListzipWithSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing ZipWithSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing MapAccumRSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing MapAccumLSym0

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

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing FoldrSym0

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

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing Foldr'Sym0

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

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing FoldlSym0

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

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing Foldl'Sym0

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

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing FoldMapSym0

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

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing ConcatMapSym0

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

Defined in Data.Singletons.Prelude.Either

Methods

sing :: Sing Either_Sym0

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

Defined in Data.Singletons.Prelude.Base

Methods

sing :: Sing FlipSym0

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

Defined in Data.Singletons.Prelude.Base

Methods

sing :: Sing (.@#@$)

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

Defined in Data.Singletons.Prelude.Functor

Methods

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

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

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)

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing Unzip4Sym0

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

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

Defined in Data.Singletons.Prelude.Base

Methods

sing :: Sing (FoldrSym2 d1 d2)

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

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)

Defined in Data.Singletons.Prelude.Maybe

Methods

sing :: Sing (Maybe_Sym2 d1 d2)

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

Defined in Data.Singletons.Prelude.Tuple

Methods

sing :: Sing (UncurrySym1 d)

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

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)

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)

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)

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)

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)

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)

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)

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)

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)

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing (ApSym1 d)

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

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

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

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

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

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

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

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

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

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

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

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

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

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)

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)

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

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

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

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

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

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (MapAccumRSym1 d)

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

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing AsumSym0

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

Defined in Data.Singletons.Prelude.Base

Methods

sing :: Sing (FlipSym1 d)

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

Defined in Data.Singletons.Prelude.Instances

Methods

sing :: Sing Tuple4Sym0

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

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)

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)

Defined in Data.Singletons.Prelude.Functor

Methods

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

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

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)

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)

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)

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)

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)

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)

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)

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)

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

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

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

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)

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)

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)

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)

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)

Defined in Data.Singletons.Prelude.Either

Methods

sing :: Sing (Either_Sym1 d b)

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

Defined in Data.Singletons.Prelude.Base

Methods

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

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

Defined in Data.Singletons.Prelude.Functor

Methods

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

SingI k2 => SingI (k2 :-> v2 :: Mapping k1 v1)

Defined in Data.NamedSOP.Type

Methods

sing :: Sing (k2 :-> v2)

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing Unzip5Sym0

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

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)

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (ZipWithSym2 d1 d2)

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

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

Defined in Data.Singletons.Prelude.Base

Methods

sing :: Sing (FlipSym2 d1 d2)

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

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing Unzip6Sym0

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

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

Defined in Data.Singletons.Prelude.Instances

Methods

sing :: Sing (Tuple7Sym6 d2 d3 d4 d5 d6 d7 g)

data family Sing (a :: k) :: Type infixr 5

The singleton kind-indexed data family.

Instances

data Sing (a :: Bool)

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)

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)

Defined in Data.Singletons.TypeLits.Internal

data Sing (n :: Nat) where

• SNat :: forall (n :: Nat). KnownNat n => Sing n

data Sing (n :: Symbol)

Defined in Data.Singletons.TypeLits.Internal

data Sing (n :: Symbol) where

• SSym :: forall (n :: Symbol). KnownSymbol n => Sing n

data Sing (a :: ())

Defined in Data.Singletons.Prelude.Instances

data Sing (a :: ()) where

• STuple0 :: forall (a :: ()). Sing ()

data Sing (a :: Void)

Defined in Data.Singletons.Prelude.Instances

data Sing (a :: Void)

data Sing (a :: All)

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)

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

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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 :: MaxInternal a)

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 (b :: MinInternal a)

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 (c :: Either a b)

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

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)

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)

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)

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)

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)

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

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)

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

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

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

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

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)