singletons-2.5.1: A framework for generating singleton types

Copyright(C) 2014 Richard Eisenberg
LicenseBSD-style (see LICENSE)
MaintainerRyan Scott
Stabilityexperimental
Portabilitynon-portable
Safe HaskellNone
LanguageHaskell2010

Data.Singletons.TypeLits

Contents

Description

Defines and exports singletons useful for the Nat and Symbol kinds.

Synopsis

Documentation

data Nat Source #

(Kind) This is the kind of type-level natural numbers.

Instances
Enum Nat Source # 
Instance details

Defined in Data.Singletons.TypeLits

Eq Nat Source # 
Instance details

Defined in Data.Singletons.TypeLits

Methods

(==) :: Nat -> Nat -> Bool Source #

(/=) :: Nat -> Nat -> Bool Source #

Num Nat Source #

This bogus Num instance is helpful for people who want to define functions over Nats that will only be used at the type level or as singletons. A correct SNum instance for Nat singletons exists.

Instance details

Defined in Data.Singletons.TypeLits

Ord Nat Source # 
Instance details

Defined in Data.Singletons.TypeLits

Methods

compare :: Nat -> Nat -> Ordering Source #

(<) :: Nat -> Nat -> Bool Source #

(<=) :: Nat -> Nat -> Bool Source #

(>) :: Nat -> Nat -> Bool Source #

(>=) :: Nat -> Nat -> Bool Source #

max :: Nat -> Nat -> Nat Source #

min :: Nat -> Nat -> Nat Source #

Show Nat Source # 
Instance details

Defined in Data.Singletons.TypeLits

SingKind Nat Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

Associated Types

type Demote Nat = (r :: Type) Source #

SDecide Nat Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

Methods

(%~) :: Sing a -> Sing b -> Decision (a :~: b) Source #

PEq Nat Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

Associated Types

type x == y :: Bool Source #

type x /= y :: Bool Source #

SEq Nat Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

Methods

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

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

SOrd Nat Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

Methods

sCompare :: Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source #

(%<) :: Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source #

(%<=) :: Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source #

(%>) :: Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source #

(%>=) :: Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source #

sMax :: Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source #

sMin :: Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source #

POrd Nat Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

Associated Types

type Compare arg arg :: Ordering Source #

type arg < arg :: Bool Source #

type arg <= arg :: Bool Source #

type arg > arg :: Bool Source #

type arg >= arg :: Bool Source #

type Max arg arg :: a Source #

type Min arg arg :: a Source #

SNum Nat Source # 
Instance details

Defined in Data.Singletons.Prelude.Num

PNum Nat Source # 
Instance details

Defined in Data.Singletons.Prelude.Num

Associated Types

type arg + arg :: a Source #

type arg - arg :: a Source #

type arg * arg :: a Source #

type Negate arg :: a Source #

type Abs arg :: a Source #

type Signum arg :: a Source #

type FromInteger arg :: a Source #

SEnum Nat Source # 
Instance details

Defined in Data.Singletons.Prelude.Enum

PEnum Nat Source # 
Instance details

Defined in Data.Singletons.Prelude.Enum

Associated Types

type Succ arg :: a Source #

type Pred arg :: a Source #

type ToEnum arg :: a Source #

type FromEnum arg :: Nat Source #

type EnumFromTo arg arg :: [a] Source #

type EnumFromThenTo arg arg arg :: [a] Source #

SShow Nat Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

PShow Nat Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

Associated Types

type ShowsPrec arg arg arg :: Symbol Source #

type Show_ arg :: Symbol Source #

type ShowList arg arg :: Symbol Source #

KnownNat n => SingI (n :: Nat) Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

Methods

sing :: Sing n Source #

Show (SNat n) Source # 
Instance details

Defined in Data.Singletons.ShowSing

Methods

showsPrec :: Int -> SNat n -> ShowS Source #

show :: SNat n -> String Source #

showList :: [SNat n] -> ShowS Source #

SingI Log2Sym0 Source # 
Instance details

Defined in Data.Singletons.TypeLits

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

Defined in Data.Singletons.TypeLits.Internal

SingI (^@#@$) Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

SingI DivSym0 Source # 
Instance details

Defined in Data.Singletons.TypeLits

SingI ModSym0 Source # 
Instance details

Defined in Data.Singletons.TypeLits

SuppressUnusedWarnings KnownNatSym0 Source # 
Instance details

Defined in Data.Singletons.TypeLits

SuppressUnusedWarnings Log2Sym0 Source # 
Instance details

Defined in Data.Singletons.TypeLits

SuppressUnusedWarnings (<=?@#@$) Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

SuppressUnusedWarnings (^@#@$) Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

SuppressUnusedWarnings DivSym0 Source # 
Instance details

Defined in Data.Singletons.TypeLits

SuppressUnusedWarnings ModSym0 Source # 
Instance details

Defined in Data.Singletons.TypeLits

SuppressUnusedWarnings QuotSym0 Source # 
Instance details

Defined in Data.Singletons.TypeLits

SuppressUnusedWarnings RemSym0 Source # 
Instance details

Defined in Data.Singletons.TypeLits

SuppressUnusedWarnings QuotRemSym0 Source # 
Instance details

Defined in Data.Singletons.TypeLits

SuppressUnusedWarnings DivModSym0 Source # 
Instance details

Defined in Data.Singletons.TypeLits

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

Defined in Data.Singletons.TypeLits.Internal

Methods

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

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

Defined in Data.Singletons.TypeLits.Internal

Methods

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

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

Defined in Data.Singletons.TypeLits

Methods

sing :: Sing (DivSym1 x) Source #

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

Defined in Data.Singletons.TypeLits

Methods

sing :: Sing (ModSym1 x) Source #

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

Defined in Data.Singletons.Prelude.List.Internal

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

Defined in Data.Singletons.Prelude.Num

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

Defined in Data.Singletons.Prelude.Enum

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

Defined in Data.Singletons.Prelude.List.Internal

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

Defined in Data.Singletons.Prelude.List.Internal

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

Defined in Data.Singletons.Prelude.List.Internal

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

Defined in Data.Singletons.Prelude.List.Internal

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

Defined in Data.Singletons.Prelude.Show

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

Defined in Data.Singletons.Prelude.List.NonEmpty

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

Defined in Data.Singletons.Prelude.List.NonEmpty

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

Defined in Data.Singletons.Prelude.List.NonEmpty

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

Defined in Data.Singletons.Prelude.Enum

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

Defined in Data.Singletons.Prelude.List.Internal

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

Defined in Data.Singletons.Prelude.List.Internal

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

Defined in Data.Singletons.Prelude.List.NonEmpty

SingI (LengthSym0 :: TyFun (NonEmpty a) Nat -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.List.NonEmpty

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

Defined in Data.Singletons.Prelude.List.Internal

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

Defined in Data.Singletons.Prelude.List.Internal

SuppressUnusedWarnings ((!!@#@$) :: TyFun [a6989586621679939336] (Nat ~> a6989586621679939336) -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

SuppressUnusedWarnings ((<=?@#@$$) a3530822107858468865 :: TyFun Nat Bool -> Type) Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

SuppressUnusedWarnings ((^@#@$$) a3530822107858468865 :: TyFun Nat Nat -> Type) Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

SuppressUnusedWarnings (DivSym1 a3530822107858468865 :: TyFun Nat Nat -> Type) Source # 
Instance details

Defined in Data.Singletons.TypeLits

SuppressUnusedWarnings (ModSym1 a3530822107858468865 :: TyFun Nat Nat -> Type) Source # 
Instance details

Defined in Data.Singletons.TypeLits

SuppressUnusedWarnings (QuotSym1 a6989586621679488500 :: TyFun Nat Nat -> Type) Source # 
Instance details

Defined in Data.Singletons.TypeLits

SuppressUnusedWarnings (RemSym1 a6989586621679488490 :: TyFun Nat Nat -> Type) Source # 
Instance details

Defined in Data.Singletons.TypeLits

SuppressUnusedWarnings (QuotRemSym1 a6989586621679488516 :: TyFun Nat (Nat, Nat) -> Type) Source # 
Instance details

Defined in Data.Singletons.TypeLits

SuppressUnusedWarnings (DivModSym1 a6989586621679488506 :: TyFun Nat (Nat, Nat) -> Type) Source # 
Instance details

Defined in Data.Singletons.TypeLits

SuppressUnusedWarnings (FromIntegerSym0 :: TyFun Nat a6989586621679506802 -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Num

SuppressUnusedWarnings (ToEnumSym0 :: TyFun Nat a6989586621679740900 -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Enum

SuppressUnusedWarnings (DropSym0 :: TyFun Nat ([a6989586621679939353] ~> [a6989586621679939353]) -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

SuppressUnusedWarnings (TakeSym0 :: TyFun Nat ([a6989586621679939354] ~> [a6989586621679939354]) -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

SuppressUnusedWarnings (SplitAtSym0 :: TyFun Nat ([a6989586621679939352] ~> ([a6989586621679939352], [a6989586621679939352])) -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

SuppressUnusedWarnings (ReplicateSym0 :: TyFun Nat (a6989586621679939338 ~> [a6989586621679939338]) -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

SuppressUnusedWarnings (ShowsPrecSym0 :: TyFun Nat (a6989586621680258583 ~> (Symbol ~> Symbol)) -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

SuppressUnusedWarnings (TakeSym0 :: TyFun Nat (NonEmpty a6989586621681099365 ~> [a6989586621681099365]) -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.List.NonEmpty

SuppressUnusedWarnings (DropSym0 :: TyFun Nat (NonEmpty a6989586621681099364 ~> [a6989586621681099364]) -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.List.NonEmpty

SuppressUnusedWarnings (SplitAtSym0 :: TyFun Nat (NonEmpty a6989586621681099363 ~> ([a6989586621681099363], [a6989586621681099363])) -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.List.NonEmpty

SuppressUnusedWarnings (FromEnumSym0 :: TyFun a6989586621679740900 Nat -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Enum

SuppressUnusedWarnings (ElemIndicesSym0 :: TyFun a6989586621679939364 ([a6989586621679939364] ~> [Nat]) -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

SuppressUnusedWarnings (ElemIndexSym0 :: TyFun a6989586621679939365 ([a6989586621679939365] ~> Maybe Nat) -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

SuppressUnusedWarnings ((!!@#@$) :: TyFun (NonEmpty a6989586621681099343) (Nat ~> a6989586621681099343) -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.List.NonEmpty

SuppressUnusedWarnings (LengthSym0 :: TyFun (NonEmpty a6989586621681099396) Nat -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.List.NonEmpty

SuppressUnusedWarnings (FindIndicesSym0 :: TyFun (a6989586621679939362 ~> Bool) ([a6989586621679939362] ~> [Nat]) -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

SuppressUnusedWarnings (FindIndexSym0 :: TyFun (a6989586621679939363 ~> Bool) ([a6989586621679939363] ~> Maybe Nat) -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

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

Defined in Data.Singletons.Prelude.List.Internal

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

Defined in Data.Singletons.Prelude.List.Internal

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

Defined in Data.Singletons.Prelude.List.Internal

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

Defined in Data.Singletons.Prelude.List.Internal

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

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

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

Defined in Data.Singletons.Prelude.List.NonEmpty

Methods

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

SApplicative m => SingI (ReplicateM_Sym0 :: TyFun Nat (m a ~> m ()) -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Monad

SApplicative m => SingI (ReplicateMSym0 :: TyFun Nat (m a ~> m [a]) -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Monad

SuppressUnusedWarnings (FindIndicesSym1 a6989586621679949249 :: TyFun [a6989586621679939362] [Nat] -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

SuppressUnusedWarnings (ElemIndicesSym1 a6989586621679949275 :: TyFun [a6989586621679939364] [Nat] -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

SuppressUnusedWarnings (FindIndexSym1 a6989586621679949283 :: TyFun [a6989586621679939363] (Maybe Nat) -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

SuppressUnusedWarnings (ElemIndexSym1 a6989586621679949291 :: TyFun [a6989586621679939365] (Maybe Nat) -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

SuppressUnusedWarnings ((!!@#@$$) a6989586621679948626 :: TyFun Nat a6989586621679939336 -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

SuppressUnusedWarnings ((!!@#@$$) a6989586621681100849 :: TyFun Nat a6989586621681099343 -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.List.NonEmpty

SuppressUnusedWarnings (ReplicateM_Sym0 :: TyFun Nat (m6989586621681203135 a6989586621681203136 ~> m6989586621681203135 ()) -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Monad

SuppressUnusedWarnings (ReplicateMSym0 :: TyFun Nat (m6989586621681203137 a6989586621681203138 ~> m6989586621681203137 [a6989586621681203138]) -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Monad

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

Defined in Data.Singletons.Prelude.Foldable

SuppressUnusedWarnings (LengthSym0 :: TyFun (t6989586621680448444 a6989586621680448460) Nat -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Foldable

type Demote Nat Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

data Sing (n :: Nat) Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

data Sing (n :: Nat) where
type Negate (a :: Nat) Source # 
Instance details

Defined in Data.Singletons.Prelude.Num

type Negate (a :: Nat) = (Error "Cannot negate a natural number" :: Nat)
type Abs (a :: Nat) Source # 
Instance details

Defined in Data.Singletons.Prelude.Num

type Abs (a :: Nat) = a
type Signum (a :: Nat) Source # 
Instance details

Defined in Data.Singletons.Prelude.Num

type Signum (a :: Nat)
type FromInteger a Source # 
Instance details

Defined in Data.Singletons.Prelude.Num

type FromInteger a = a
type Succ (a :: Nat) Source # 
Instance details

Defined in Data.Singletons.Prelude.Enum

type Succ (a :: Nat)
type Pred (a :: Nat) Source # 
Instance details

Defined in Data.Singletons.Prelude.Enum

type Pred (a :: Nat)
type ToEnum a Source # 
Instance details

Defined in Data.Singletons.Prelude.Enum

type ToEnum a
type FromEnum (a :: Nat) Source # 
Instance details

Defined in Data.Singletons.Prelude.Enum

type FromEnum (a :: Nat)
type Show_ (arg :: Nat) Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

type Show_ (arg :: Nat)
type (x :: Nat) == (y :: Nat) Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

type (x :: Nat) == (y :: Nat) = DefaultEq x y
type (x :: Nat) /= (y :: Nat) Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

type (x :: Nat) /= (y :: Nat) = Not (x == y)
type Compare (a :: Nat) (b :: Nat) Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

type Compare (a :: Nat) (b :: Nat) = CmpNat a b
type (arg1 :: Nat) < (arg2 :: Nat) Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

type (arg1 :: Nat) < (arg2 :: Nat)
type (arg1 :: Nat) <= (arg2 :: Nat) Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

type (arg1 :: Nat) <= (arg2 :: Nat)
type (arg1 :: Nat) > (arg2 :: Nat) Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

type (arg1 :: Nat) > (arg2 :: Nat)
type (arg1 :: Nat) >= (arg2 :: Nat) Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

type (arg1 :: Nat) >= (arg2 :: Nat)
type Max (arg1 :: Nat) (arg2 :: Nat) Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

type Max (arg1 :: Nat) (arg2 :: Nat)
type Min (arg1 :: Nat) (arg2 :: Nat) Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

type Min (arg1 :: Nat) (arg2 :: Nat)
type (a :: Nat) + (b :: Nat) Source # 
Instance details

Defined in Data.Singletons.Prelude.Num

type (a :: Nat) + (b :: Nat) = a + b
type (a :: Nat) - (b :: Nat) Source # 
Instance details

Defined in Data.Singletons.Prelude.Num

type (a :: Nat) - (b :: Nat) = a - b
type (a :: Nat) * (b :: Nat) Source # 
Instance details

Defined in Data.Singletons.Prelude.Num

type (a :: Nat) * (b :: Nat) = a * b
type EnumFromTo (a1 :: Nat) (a2 :: Nat) Source # 
Instance details

Defined in Data.Singletons.Prelude.Enum

type EnumFromTo (a1 :: Nat) (a2 :: Nat)
type ShowList (arg1 :: [Nat]) arg2 Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

type ShowList (arg1 :: [Nat]) arg2
type Apply KnownNatSym0 (n6989586621679469170 :: Nat) Source # 
Instance details

Defined in Data.Singletons.TypeLits

type Apply KnownNatSym0 (n6989586621679469170 :: Nat) = KnownNat n6989586621679469170
type Apply Log2Sym0 (a3530822107858468865 :: Nat) Source # 
Instance details

Defined in Data.Singletons.TypeLits

type Apply Log2Sym0 (a3530822107858468865 :: Nat) = Log2 a3530822107858468865
type EnumFromThenTo (a1 :: Nat) (a2 :: Nat) (a3 :: Nat) Source # 
Instance details

Defined in Data.Singletons.Prelude.Enum

type EnumFromThenTo (a1 :: Nat) (a2 :: Nat) (a3 :: Nat)
type ShowsPrec _ (n :: Nat) x Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

type ShowsPrec _ (n :: Nat) x
type Apply ((<=?@#@$$) a3530822107858468865 :: TyFun Nat Bool -> Type) (b3530822107858468866 :: Nat) Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

type Apply ((<=?@#@$$) a3530822107858468865 :: TyFun Nat Bool -> Type) (b3530822107858468866 :: Nat) = a3530822107858468865 <=? b3530822107858468866
type Apply ((^@#@$$) a3530822107858468865 :: TyFun Nat Nat -> Type) (b3530822107858468866 :: Nat) Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

type Apply ((^@#@$$) a3530822107858468865 :: TyFun Nat Nat -> Type) (b3530822107858468866 :: Nat) = a3530822107858468865 ^ b3530822107858468866
type Apply (DivSym1 a3530822107858468865 :: TyFun Nat Nat -> Type) (b3530822107858468866 :: Nat) Source # 
Instance details

Defined in Data.Singletons.TypeLits

type Apply (DivSym1 a3530822107858468865 :: TyFun Nat Nat -> Type) (b3530822107858468866 :: Nat) = Div a3530822107858468865 b3530822107858468866
type Apply (ModSym1 a3530822107858468865 :: TyFun Nat Nat -> Type) (b3530822107858468866 :: Nat) Source # 
Instance details

Defined in Data.Singletons.TypeLits

type Apply (ModSym1 a3530822107858468865 :: TyFun Nat Nat -> Type) (b3530822107858468866 :: Nat) = Mod a3530822107858468865 b3530822107858468866
type Apply (QuotSym1 a6989586621679488500 :: TyFun Nat Nat -> Type) (a6989586621679488501 :: Nat) Source # 
Instance details

Defined in Data.Singletons.TypeLits

type Apply (QuotSym1 a6989586621679488500 :: TyFun Nat Nat -> Type) (a6989586621679488501 :: Nat) = Quot a6989586621679488500 a6989586621679488501
type Apply (RemSym1 a6989586621679488490 :: TyFun Nat Nat -> Type) (a6989586621679488491 :: Nat) Source # 
Instance details

Defined in Data.Singletons.TypeLits

type Apply (RemSym1 a6989586621679488490 :: TyFun Nat Nat -> Type) (a6989586621679488491 :: Nat) = Rem a6989586621679488490 a6989586621679488491
type Apply (FromEnumSym0 :: TyFun a Nat -> Type) (arg6989586621679741190 :: a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Enum

type Apply (FromEnumSym0 :: TyFun a Nat -> Type) (arg6989586621679741190 :: a) = FromEnum arg6989586621679741190
type Apply (FromIntegerSym0 :: TyFun Nat k2 -> Type) (arg6989586621679506840 :: Nat) Source # 
Instance details

Defined in Data.Singletons.Prelude.Num

type Apply (FromIntegerSym0 :: TyFun Nat k2 -> Type) (arg6989586621679506840 :: Nat) = (FromInteger arg6989586621679506840 :: k2)
type Apply (ToEnumSym0 :: TyFun Nat k2 -> Type) (arg6989586621679741188 :: Nat) Source # 
Instance details

Defined in Data.Singletons.Prelude.Enum

type Apply (ToEnumSym0 :: TyFun Nat k2 -> Type) (arg6989586621679741188 :: Nat) = (ToEnum arg6989586621679741188 :: k2)
type Apply ((!!@#@$$) a6989586621679948626 :: TyFun Nat a -> Type) (a6989586621679948627 :: Nat) Source # 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

type Apply ((!!@#@$$) a6989586621679948626 :: TyFun Nat a -> Type) (a6989586621679948627 :: Nat) = a6989586621679948626 !! a6989586621679948627
type Apply ((!!@#@$$) a6989586621681100849 :: TyFun Nat a -> Type) (a6989586621681100850 :: Nat) Source # 
Instance details

Defined in Data.Singletons.Prelude.List.NonEmpty

type Apply ((!!@#@$$) a6989586621681100849 :: TyFun Nat a -> Type) (a6989586621681100850 :: Nat) = a6989586621681100849 !! a6989586621681100850
type Apply (LengthSym0 :: TyFun (NonEmpty a) Nat -> Type) (a6989586621681101279 :: NonEmpty a) Source # 
Instance details

Defined in Data.Singletons.Prelude.List.NonEmpty

type Apply (LengthSym0 :: TyFun (NonEmpty a) Nat -> Type) (a6989586621681101279 :: NonEmpty a) = Length a6989586621681101279
type Apply (LengthSym0 :: TyFun (t a) Nat -> Type) (arg6989586621680449109 :: t a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Foldable

type Apply (LengthSym0 :: TyFun (t a) Nat -> Type) (arg6989586621680449109 :: t a) = Length arg6989586621680449109
type Apply (FindIndicesSym1 a6989586621679949249 :: TyFun [a] [Nat] -> Type) (a6989586621679949250 :: [a]) Source # 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

type Apply (FindIndicesSym1 a6989586621679949249 :: TyFun [a] [Nat] -> Type) (a6989586621679949250 :: [a]) = FindIndices a6989586621679949249 a6989586621679949250
type Apply (ElemIndicesSym1 a6989586621679949275 :: TyFun [a] [Nat] -> Type) (a6989586621679949276 :: [a]) Source # 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

type Apply (ElemIndicesSym1 a6989586621679949275 :: TyFun [a] [Nat] -> Type) (a6989586621679949276 :: [a]) = ElemIndices a6989586621679949275 a6989586621679949276
type Apply (FindIndexSym1 a6989586621679949283 :: TyFun [a] (Maybe Nat) -> Type) (a6989586621679949284 :: [a]) Source # 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

type Apply (FindIndexSym1 a6989586621679949283 :: TyFun [a] (Maybe Nat) -> Type) (a6989586621679949284 :: [a]) = FindIndex a6989586621679949283 a6989586621679949284
type Apply (ElemIndexSym1 a6989586621679949291 :: TyFun [a] (Maybe Nat) -> Type) (a6989586621679949292 :: [a]) Source # 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

type Apply (ElemIndexSym1 a6989586621679949291 :: TyFun [a] (Maybe Nat) -> Type) (a6989586621679949292 :: [a]) = ElemIndex a6989586621679949291 a6989586621679949292
type Apply (<=?@#@$) (a3530822107858468865 :: Nat) Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

type Apply (<=?@#@$) (a3530822107858468865 :: Nat) = (<=?@#@$$) a3530822107858468865
type Apply (^@#@$) (a3530822107858468865 :: Nat) Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

type Apply (^@#@$) (a3530822107858468865 :: Nat) = (^@#@$$) a3530822107858468865
type Apply DivSym0 (a3530822107858468865 :: Nat) Source # 
Instance details

Defined in Data.Singletons.TypeLits

type Apply DivSym0 (a3530822107858468865 :: Nat) = DivSym1 a3530822107858468865
type Apply ModSym0 (a3530822107858468865 :: Nat) Source # 
Instance details

Defined in Data.Singletons.TypeLits

type Apply ModSym0 (a3530822107858468865 :: Nat) = ModSym1 a3530822107858468865
type Apply QuotSym0 (a6989586621679488500 :: Nat) Source # 
Instance details

Defined in Data.Singletons.TypeLits

type Apply QuotSym0 (a6989586621679488500 :: Nat) = QuotSym1 a6989586621679488500
type Apply RemSym0 (a6989586621679488490 :: Nat) Source # 
Instance details

Defined in Data.Singletons.TypeLits

type Apply RemSym0 (a6989586621679488490 :: Nat) = RemSym1 a6989586621679488490
type Apply QuotRemSym0 (a6989586621679488516 :: Nat) Source # 
Instance details

Defined in Data.Singletons.TypeLits

type Apply QuotRemSym0 (a6989586621679488516 :: Nat) = QuotRemSym1 a6989586621679488516
type Apply DivModSym0 (a6989586621679488506 :: Nat) Source # 
Instance details

Defined in Data.Singletons.TypeLits

type Apply DivModSym0 (a6989586621679488506 :: Nat) = DivModSym1 a6989586621679488506
type Apply (QuotRemSym1 a6989586621679488516 :: TyFun Nat (Nat, Nat) -> Type) (a6989586621679488517 :: Nat) Source # 
Instance details

Defined in Data.Singletons.TypeLits

type Apply (QuotRemSym1 a6989586621679488516 :: TyFun Nat (Nat, Nat) -> Type) (a6989586621679488517 :: Nat) = QuotRem a6989586621679488516 a6989586621679488517
type Apply (DivModSym1 a6989586621679488506 :: TyFun Nat (Nat, Nat) -> Type) (a6989586621679488507 :: Nat) Source # 
Instance details

Defined in Data.Singletons.TypeLits

type Apply (DivModSym1 a6989586621679488506 :: TyFun Nat (Nat, Nat) -> Type) (a6989586621679488507 :: Nat) = DivMod a6989586621679488506 a6989586621679488507
type Apply (DropSym0 :: TyFun Nat ([a6989586621679939353] ~> [a6989586621679939353]) -> Type) (a6989586621679948722 :: Nat) Source # 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

type Apply (DropSym0 :: TyFun Nat ([a6989586621679939353] ~> [a6989586621679939353]) -> Type) (a6989586621679948722 :: Nat) = (DropSym1 a6989586621679948722 a6989586621679939353 :: TyFun [a6989586621679939353] [a6989586621679939353] -> Type)
type Apply (TakeSym0 :: TyFun Nat ([a6989586621679939354] ~> [a6989586621679939354]) -> Type) (a6989586621679948736 :: Nat) Source # 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

type Apply (TakeSym0 :: TyFun Nat ([a6989586621679939354] ~> [a6989586621679939354]) -> Type) (a6989586621679948736 :: Nat) = (TakeSym1 a6989586621679948736 a6989586621679939354 :: TyFun [a6989586621679939354] [a6989586621679939354] -> Type)
type Apply (SplitAtSym0 :: TyFun Nat ([a6989586621679939352] ~> ([a6989586621679939352], [a6989586621679939352])) -> Type) (a6989586621679948750 :: Nat) Source # 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

type Apply (SplitAtSym0 :: TyFun Nat ([a6989586621679939352] ~> ([a6989586621679939352], [a6989586621679939352])) -> Type) (a6989586621679948750 :: Nat) = (SplitAtSym1 a6989586621679948750 a6989586621679939352 :: TyFun [a6989586621679939352] ([a6989586621679939352], [a6989586621679939352]) -> Type)
type Apply (ElemIndicesSym0 :: TyFun a6989586621679939364 ([a6989586621679939364] ~> [Nat]) -> Type) (a6989586621679949275 :: a6989586621679939364) Source # 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

type Apply (ElemIndicesSym0 :: TyFun a6989586621679939364 ([a6989586621679939364] ~> [Nat]) -> Type) (a6989586621679949275 :: a6989586621679939364) = ElemIndicesSym1 a6989586621679949275
type Apply (ElemIndexSym0 :: TyFun a6989586621679939365 ([a6989586621679939365] ~> Maybe Nat) -> Type) (a6989586621679949291 :: a6989586621679939365) Source # 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

type Apply (ElemIndexSym0 :: TyFun a6989586621679939365 ([a6989586621679939365] ~> Maybe Nat) -> Type) (a6989586621679949291 :: a6989586621679939365) = ElemIndexSym1 a6989586621679949291
type Apply (ReplicateSym0 :: TyFun Nat (a6989586621679939338 ~> [a6989586621679939338]) -> Type) (a6989586621679948640 :: Nat) Source # 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

type Apply (ReplicateSym0 :: TyFun Nat (a6989586621679939338 ~> [a6989586621679939338]) -> Type) (a6989586621679948640 :: Nat) = (ReplicateSym1 a6989586621679948640 a6989586621679939338 :: TyFun a6989586621679939338 [a6989586621679939338] -> Type)
type Apply (ShowsPrecSym0 :: TyFun Nat (a6989586621680258583 ~> (Symbol ~> Symbol)) -> Type) (arg6989586621680260533 :: Nat) Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

type Apply (ShowsPrecSym0 :: TyFun Nat (a6989586621680258583 ~> (Symbol ~> Symbol)) -> Type) (arg6989586621680260533 :: Nat) = (ShowsPrecSym1 arg6989586621680260533 a6989586621680258583 :: TyFun a6989586621680258583 (Symbol ~> Symbol) -> Type)
type Apply (TakeSym0 :: TyFun Nat (NonEmpty a6989586621681099365 ~> [a6989586621681099365]) -> Type) (a6989586621681101009 :: Nat) Source # 
Instance details

Defined in Data.Singletons.Prelude.List.NonEmpty

type Apply (TakeSym0 :: TyFun Nat (NonEmpty a6989586621681099365 ~> [a6989586621681099365]) -> Type) (a6989586621681101009 :: Nat) = (TakeSym1 a6989586621681101009 a6989586621681099365 :: TyFun (NonEmpty a6989586621681099365) [a6989586621681099365] -> Type)
type Apply (DropSym0 :: TyFun Nat (NonEmpty a6989586621681099364 ~> [a6989586621681099364]) -> Type) (a6989586621681101017 :: Nat) Source # 
Instance details

Defined in Data.Singletons.Prelude.List.NonEmpty

type Apply (DropSym0 :: TyFun Nat (NonEmpty a6989586621681099364 ~> [a6989586621681099364]) -> Type) (a6989586621681101017 :: Nat) = (DropSym1 a6989586621681101017 a6989586621681099364 :: TyFun (NonEmpty a6989586621681099364) [a6989586621681099364] -> Type)
type Apply (SplitAtSym0 :: TyFun Nat (NonEmpty a6989586621681099363 ~> ([a6989586621681099363], [a6989586621681099363])) -> Type) (a6989586621681101025 :: Nat) Source # 
Instance details

Defined in Data.Singletons.Prelude.List.NonEmpty

type Apply (SplitAtSym0 :: TyFun Nat (NonEmpty a6989586621681099363 ~> ([a6989586621681099363], [a6989586621681099363])) -> Type) (a6989586621681101025 :: Nat) = (SplitAtSym1 a6989586621681101025 a6989586621681099363 :: TyFun (NonEmpty a6989586621681099363) ([a6989586621681099363], [a6989586621681099363]) -> Type)
type Apply (ReplicateM_Sym0 :: TyFun Nat (m6989586621681203135 a6989586621681203136 ~> m6989586621681203135 ()) -> Type) (a6989586621681203511 :: Nat) Source # 
Instance details

Defined in Data.Singletons.Prelude.Monad

type Apply (ReplicateM_Sym0 :: TyFun Nat (m6989586621681203135 a6989586621681203136 ~> m6989586621681203135 ()) -> Type) (a6989586621681203511 :: Nat) = (ReplicateM_Sym1 a6989586621681203511 a6989586621681203136 m6989586621681203135 :: TyFun (m6989586621681203135 a6989586621681203136) (m6989586621681203135 ()) -> Type)
type Apply (ReplicateMSym0 :: TyFun Nat (m6989586621681203137 a6989586621681203138 ~> m6989586621681203137 [a6989586621681203138]) -> Type) (a6989586621681203530 :: Nat) Source # 
Instance details

Defined in Data.Singletons.Prelude.Monad

type Apply (ReplicateMSym0 :: TyFun Nat (m6989586621681203137 a6989586621681203138 ~> m6989586621681203137 [a6989586621681203138]) -> Type) (a6989586621681203530 :: Nat) = (ReplicateMSym1 a6989586621681203530 a6989586621681203138 m6989586621681203137 :: TyFun (m6989586621681203137 a6989586621681203138) (m6989586621681203137 [a6989586621681203138]) -> Type)
type Apply ((!!@#@$) :: TyFun [a6989586621679939336] (Nat ~> a6989586621679939336) -> Type) (a6989586621679948626 :: [a6989586621679939336]) Source # 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

type Apply ((!!@#@$) :: TyFun [a6989586621679939336] (Nat ~> a6989586621679939336) -> Type) (a6989586621679948626 :: [a6989586621679939336]) = (!!@#@$$) a6989586621679948626
type Apply ((!!@#@$) :: TyFun (NonEmpty a6989586621681099343) (Nat ~> a6989586621681099343) -> Type) (a6989586621681100849 :: NonEmpty a6989586621681099343) Source # 
Instance details

Defined in Data.Singletons.Prelude.List.NonEmpty

type Apply ((!!@#@$) :: TyFun (NonEmpty a6989586621681099343) (Nat ~> a6989586621681099343) -> Type) (a6989586621681100849 :: NonEmpty a6989586621681099343) = (!!@#@$$) a6989586621681100849
type Apply (FindIndicesSym0 :: TyFun (a6989586621679939362 ~> Bool) ([a6989586621679939362] ~> [Nat]) -> Type) (a6989586621679949249 :: a6989586621679939362 ~> Bool) Source # 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

type Apply (FindIndicesSym0 :: TyFun (a6989586621679939362 ~> Bool) ([a6989586621679939362] ~> [Nat]) -> Type) (a6989586621679949249 :: a6989586621679939362 ~> Bool) = FindIndicesSym1 a6989586621679949249
type Apply (FindIndexSym0 :: TyFun (a6989586621679939363 ~> Bool) ([a6989586621679939363] ~> Maybe Nat) -> Type) (a6989586621679949283 :: a6989586621679939363 ~> Bool) Source # 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

type Apply (FindIndexSym0 :: TyFun (a6989586621679939363 ~> Bool) ([a6989586621679939363] ~> Maybe Nat) -> Type) (a6989586621679949283 :: a6989586621679939363 ~> Bool) = FindIndexSym1 a6989586621679949283

data Symbol Source #

(Kind) This is the kind of type-level symbols. Declared here because class IP needs it

Instances
Eq Symbol Source #

This bogus instance is helpful for people who want to define functions over Symbols that will only be used at the type level or as singletons.

Instance details

Defined in Data.Singletons.TypeLits

Ord Symbol Source # 
Instance details

Defined in Data.Singletons.TypeLits

Show Symbol Source # 
Instance details

Defined in Data.Singletons.TypeLits

IsString Symbol Source # 
Instance details

Defined in Data.Singletons.TypeLits

Semigroup Symbol Source # 
Instance details

Defined in Data.Singletons.TypeLits

Monoid Symbol Source # 
Instance details

Defined in Data.Singletons.TypeLits

SingKind Symbol

Since: base-4.9.0.0

Instance details

Defined in GHC.Generics

Associated Types

type DemoteRep Symbol :: Type

Methods

fromSing :: Sing a -> DemoteRep Symbol

SingKind Symbol Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

Associated Types

type Demote Symbol = (r :: Type) Source #

SingKind PErrorMessage Source # 
Instance details

Defined in Data.Singletons.TypeError

Associated Types

type Demote PErrorMessage = (r :: Type) Source #

SDecide Symbol Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

Methods

(%~) :: Sing a -> Sing b -> Decision (a :~: b) Source #

PEq Symbol Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

Associated Types

type x == y :: Bool Source #

type x /= y :: Bool Source #

SEq Symbol Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

Methods

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

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

SOrd Symbol Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

Methods

sCompare :: Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source #

(%<) :: Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source #

(%<=) :: Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source #

(%>) :: Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source #

(%>=) :: Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source #

sMax :: Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source #

sMin :: Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source #

POrd Symbol Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

Associated Types

type Compare arg arg :: Ordering Source #

type arg < arg :: Bool Source #

type arg <= arg :: Bool Source #

type arg > arg :: Bool Source #

type arg >= arg :: Bool Source #

type Max arg arg :: a Source #

type Min arg arg :: a Source #

SSemigroup Symbol Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

(%<>) :: Sing t -> Sing t -> Sing (Apply (Apply (<>@#@$) t) t) Source #

sSconcat :: Sing t -> Sing (Apply SconcatSym0 t) Source #

PSemigroup Symbol Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

Associated Types

type arg <> arg :: a Source #

type Sconcat arg :: a Source #

SShow Symbol Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

PShow Symbol Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

Associated Types

type ShowsPrec arg arg arg :: Symbol Source #

type Show_ arg :: Symbol Source #

type ShowList arg arg :: Symbol Source #

SMonoid Symbol Source # 
Instance details

Defined in Data.Singletons.Prelude.Monoid

PMonoid Symbol Source # 
Instance details

Defined in Data.Singletons.Prelude.Monoid

Associated Types

type Mempty :: a Source #

type Mappend arg arg :: a Source #

type Mconcat arg :: a Source #

SIsString Symbol Source # 
Instance details

Defined in Data.Singletons.Prelude.IsString

PIsString Symbol Source # 
Instance details

Defined in Data.Singletons.Prelude.IsString

Associated Types

type FromString arg :: a Source #

KnownSymbol a => SingI (a :: Symbol)

Since: base-4.9.0.0

Instance details

Defined in GHC.Generics

Methods

sing :: Sing a

KnownSymbol n => SingI (n :: Symbol) Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

Methods

sing :: Sing n Source #

SingI t => SingI (Text t :: ErrorMessage' Symbol) Source # 
Instance details

Defined in Data.Singletons.TypeError

Methods

sing :: Sing (Text t) Source #

SingI ty => SingI (ShowType ty :: ErrorMessage' Symbol) Source # 
Instance details

Defined in Data.Singletons.TypeError

Methods

sing :: Sing (ShowType ty) Source #

(SingI e1, SingI e2) => SingI (e1 :<>: e2 :: ErrorMessage' Symbol) Source # 
Instance details

Defined in Data.Singletons.TypeError

Methods

sing :: Sing (e1 :<>: e2) Source #

(SingI e1, SingI e2) => SingI (e1 :$$: e2 :: ErrorMessage' Symbol) Source # 
Instance details

Defined in Data.Singletons.TypeError

Methods

sing :: Sing (e1 :$$: e2) Source #

Show (SSymbol s) Source # 
Instance details

Defined in Data.Singletons.ShowSing

SingI ShowParenSym0 Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

SingI UnlinesSym0 Source # 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

SingI UnwordsSym0 Source # 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

SingI ShowCommaSpaceSym0 Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

SingI ShowSpaceSym0 Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

SingI ShowCharSym0 Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

SingI ShowStringSym0 Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

SuppressUnusedWarnings ShowParenSym0 Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

SuppressUnusedWarnings UnlinesSym0 Source # 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

SuppressUnusedWarnings UnwordsSym0 Source # 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

SuppressUnusedWarnings KnownSymbolSym0 Source # 
Instance details

Defined in Data.Singletons.TypeLits

SuppressUnusedWarnings ShowCommaSpaceSym0 Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

SuppressUnusedWarnings ShowSpaceSym0 Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

SuppressUnusedWarnings ShowCharSym0 Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

SuppressUnusedWarnings ShowStringSym0 Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

SingI (TypeErrorSym0 :: TyFun PErrorMessage b6989586621681254403 -> Type) Source # 
Instance details

Defined in Data.Singletons.TypeError

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

Defined in Data.Singletons.Prelude.Show

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

Defined in Data.Singletons.Prelude.Show

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

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing (ShowCharSym1 d) Source #

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

Defined in Data.Singletons.Prelude.Show

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

Defined in Data.Singletons.Prelude.IsString

SingI (TextSym0 :: TyFun Symbol (ErrorMessage' Symbol) -> Type) Source # 
Instance details

Defined in Data.Singletons.TypeError

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

Defined in Data.Singletons.Prelude.Show

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

Defined in Data.Singletons.Prelude.Show

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

Defined in Data.Singletons.Prelude.Show

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

Defined in Data.Singletons.Prelude.Show

SingI ((:$$:@#@$) :: TyFun (ErrorMessage' Symbol) (ErrorMessage' Symbol ~> ErrorMessage' Symbol) -> Type) Source # 
Instance details

Defined in Data.Singletons.TypeError

SingI ((:<>:@#@$) :: TyFun (ErrorMessage' Symbol) (ErrorMessage' Symbol ~> ErrorMessage' Symbol) -> Type) Source # 
Instance details

Defined in Data.Singletons.TypeError

SuppressUnusedWarnings (ShowListSym0 :: TyFun [a6989586621680258583] (Symbol ~> Symbol) -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

SuppressUnusedWarnings (ShowsPrecSym0 :: TyFun Nat (a6989586621680258583 ~> (Symbol ~> Symbol)) -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

SuppressUnusedWarnings (ShowCharSym1 a6989586621680260467 :: TyFun Symbol Symbol -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

SuppressUnusedWarnings (ShowStringSym1 a6989586621680260452 :: TyFun Symbol Symbol -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

SuppressUnusedWarnings (FromStringSym0 :: TyFun Symbol a6989586621681192029 -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.IsString

SuppressUnusedWarnings (Show_Sym0 :: TyFun a6989586621680258583 Symbol -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

SuppressUnusedWarnings (ShowsSym0 :: TyFun a6989586621680258568 (Symbol ~> Symbol) -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

SuppressUnusedWarnings (ShowParenSym1 a6989586621680260473 :: TyFun (Symbol ~> Symbol) (Symbol ~> Symbol) -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

SuppressUnusedWarnings (ShowListWithSym0 :: TyFun (a6989586621680258567 ~> (Symbol ~> Symbol)) ([a6989586621680258567] ~> (Symbol ~> Symbol)) -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

SuppressUnusedWarnings (TypeErrorSym0 :: TyFun PErrorMessage b6989586621681254403 -> Type) Source # 
Instance details

Defined in Data.Singletons.TypeError

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

Defined in Data.Singletons.Prelude.Show

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

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing (ShowListSym1 d) Source #

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

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing (ShowsSym1 d) Source #

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

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing (ShowParenSym2 d1 d2) Source #

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

Defined in Data.Singletons.TypeLits.Internal

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

Defined in Data.Singletons.TypeLits.Internal

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

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing (ShowsPrecSym1 d a) Source #

SingI (ShowTypeSym0 :: TyFun t (ErrorMessage' Symbol) -> Type) Source # 
Instance details

Defined in Data.Singletons.TypeError

SingI x => SingI ((:$$:@#@$$) x :: TyFun (ErrorMessage' Symbol) (ErrorMessage' Symbol) -> Type) Source # 
Instance details

Defined in Data.Singletons.TypeError

Methods

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

SingI x => SingI ((:<>:@#@$$) x :: TyFun (ErrorMessage' Symbol) (ErrorMessage' Symbol) -> Type) Source # 
Instance details

Defined in Data.Singletons.TypeError

Methods

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

SuppressUnusedWarnings (ShowListWithSym1 a6989586621680260505 :: TyFun [a6989586621680258567] (Symbol ~> Symbol) -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

SuppressUnusedWarnings (ShowListSym1 arg6989586621680260541 :: TyFun Symbol Symbol -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

SuppressUnusedWarnings (ShowsSym1 a6989586621680260525 :: TyFun Symbol Symbol -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

SuppressUnusedWarnings (ShowParenSym2 a6989586621680260474 a6989586621680260473 :: TyFun Symbol Symbol -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

SuppressUnusedWarnings (ShowsPrecSym1 arg6989586621680260533 a6989586621680258583 :: TyFun a6989586621680258583 (Symbol ~> Symbol) -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

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

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing (ShowsPrecSym2 d1 d2) Source #

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

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing (ShowListWithSym2 d1 d2) Source #

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

Defined in Data.Singletons.Prelude.Monad.Internal

SingI (TyCon1 (Text :: Symbol -> ErrorMessage' Symbol)) Source # 
Instance details

Defined in Data.Singletons.TypeError

Methods

sing :: Sing (TyCon1 Text) Source #

SingI (TyCon1 (ShowType :: t -> ErrorMessage' Symbol) :: t ~> ErrorMessage' Symbol) Source # 
Instance details

Defined in Data.Singletons.TypeError

SingI x => SingI (TyCon1 ((:<>:) x) :: ErrorMessage' Symbol ~> ErrorMessage' Symbol) Source # 
Instance details

Defined in Data.Singletons.TypeError

Methods

sing :: Sing (TyCon1 ((:<>:) x)) Source #

SingI x => SingI (TyCon1 ((:$$:) x) :: ErrorMessage' Symbol ~> ErrorMessage' Symbol) Source # 
Instance details

Defined in Data.Singletons.TypeError

Methods

sing :: Sing (TyCon1 ((:$$:) x)) Source #

SuppressUnusedWarnings (ShowsPrecSym2 arg6989586621680260534 arg6989586621680260533 :: TyFun Symbol Symbol -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

SuppressUnusedWarnings (ShowListWithSym2 a6989586621680260506 a6989586621680260505 :: TyFun Symbol Symbol -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

SuppressUnusedWarnings (FailSym0 :: TyFun Symbol (m6989586621679545990 a6989586621679545996) -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Monad.Internal

SingI (TyCon2 ((:<>:) :: ErrorMessage' Symbol -> ErrorMessage' Symbol -> ErrorMessage' Symbol)) Source # 
Instance details

Defined in Data.Singletons.TypeError

SingI (TyCon2 ((:$$:) :: ErrorMessage' Symbol -> ErrorMessage' Symbol -> ErrorMessage' Symbol)) Source # 
Instance details

Defined in Data.Singletons.TypeError

data Sing (s :: Symbol) 
Instance details

Defined in GHC.Generics

data Sing (s :: Symbol) where
type DemoteRep Symbol 
Instance details

Defined in GHC.Generics

type DemoteRep Symbol = String
type Demote Symbol Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

type Demote PErrorMessage Source # 
Instance details

Defined in Data.Singletons.TypeError

data Sing (n :: Symbol) Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

data Sing (n :: Symbol) where
data Sing (a :: PErrorMessage) Source # 
Instance details

Defined in Data.Singletons.TypeError

data Sing (a :: PErrorMessage) where
type Mempty Source # 
Instance details

Defined in Data.Singletons.Prelude.Monoid

type Mempty
type Sconcat (arg :: NonEmpty Symbol) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

type Sconcat (arg :: NonEmpty Symbol)
type Show_ (arg :: Symbol) Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

type Show_ (arg :: Symbol)
type Mconcat (arg :: [Symbol]) Source # 
Instance details

Defined in Data.Singletons.Prelude.Monoid

type Mconcat (arg :: [Symbol])
type FromString a Source # 
Instance details

Defined in Data.Singletons.Prelude.IsString

type FromString a = a
type (x :: Symbol) == (y :: Symbol) Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

type (x :: Symbol) == (y :: Symbol) = DefaultEq x y
type (x :: Symbol) /= (y :: Symbol) Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

type (x :: Symbol) /= (y :: Symbol) = Not (x == y)
type Compare (a :: Symbol) (b :: Symbol) Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

type Compare (a :: Symbol) (b :: Symbol) = CmpSymbol a b
type (arg1 :: Symbol) < (arg2 :: Symbol) Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

type (arg1 :: Symbol) < (arg2 :: Symbol)
type (arg1 :: Symbol) <= (arg2 :: Symbol) Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

type (arg1 :: Symbol) <= (arg2 :: Symbol)
type (arg1 :: Symbol) > (arg2 :: Symbol) Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

type (arg1 :: Symbol) > (arg2 :: Symbol)
type (arg1 :: Symbol) >= (arg2 :: Symbol) Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

type (arg1 :: Symbol) >= (arg2 :: Symbol)
type Max (arg1 :: Symbol) (arg2 :: Symbol) Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

type Max (arg1 :: Symbol) (arg2 :: Symbol)
type Min (arg1 :: Symbol) (arg2 :: Symbol) Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

type Min (arg1 :: Symbol) (arg2 :: Symbol)
type (a :: Symbol) <> (b :: Symbol) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

type (a :: Symbol) <> (b :: Symbol) = AppendSymbol a b
type ShowList (arg1 :: [Symbol]) arg2 Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

type ShowList (arg1 :: [Symbol]) arg2
type Mappend (arg1 :: Symbol) (arg2 :: Symbol) Source # 
Instance details

Defined in Data.Singletons.Prelude.Monoid

type Mappend (arg1 :: Symbol) (arg2 :: Symbol)
type Apply KnownSymbolSym0 (n6989586621679469110 :: Symbol) Source # 
Instance details

Defined in Data.Singletons.TypeLits

type Apply KnownSymbolSym0 (n6989586621679469110 :: Symbol) = KnownSymbol n6989586621679469110
type Apply ShowCommaSpaceSym0 (a6989586621680260460 :: Symbol) Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

type Apply ShowCommaSpaceSym0 (a6989586621680260460 :: Symbol) = ShowCommaSpace a6989586621680260460
type Apply ShowSpaceSym0 (a6989586621680260439 :: Symbol) Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

type Apply ShowSpaceSym0 (a6989586621680260439 :: Symbol) = ShowSpace a6989586621680260439
type ShowsPrec a1 (a2 :: Symbol) a3 Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

type ShowsPrec a1 (a2 :: Symbol) a3
type Apply (ShowCharSym1 a6989586621680260467 :: TyFun Symbol Symbol -> Type) (a6989586621680260468 :: Symbol) Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

type Apply (ShowCharSym1 a6989586621680260467 :: TyFun Symbol Symbol -> Type) (a6989586621680260468 :: Symbol) = ShowChar a6989586621680260467 a6989586621680260468
type Apply (ShowStringSym1 a6989586621680260452 :: TyFun Symbol Symbol -> Type) (a6989586621680260453 :: Symbol) Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

type Apply (ShowStringSym1 a6989586621680260452 :: TyFun Symbol Symbol -> Type) (a6989586621680260453 :: Symbol) = ShowString a6989586621680260452 a6989586621680260453
type Apply (Show_Sym0 :: TyFun a Symbol -> Type) (arg6989586621680260539 :: a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

type Apply (Show_Sym0 :: TyFun a Symbol -> Type) (arg6989586621680260539 :: a) = Show_ arg6989586621680260539
type Apply (FromStringSym0 :: TyFun Symbol k2 -> Type) (arg6989586621681192065 :: Symbol) Source # 
Instance details

Defined in Data.Singletons.Prelude.IsString

type Apply (FromStringSym0 :: TyFun Symbol k2 -> Type) (arg6989586621681192065 :: Symbol) = (FromString arg6989586621681192065 :: k2)
type Apply (TypeErrorSym0 :: TyFun PErrorMessage k2 -> Type) (a6989586621681254404 :: PErrorMessage) Source # 
Instance details

Defined in Data.Singletons.TypeError

type Apply (TypeErrorSym0 :: TyFun PErrorMessage k2 -> Type) (a6989586621681254404 :: PErrorMessage) = (TypeError a6989586621681254404 :: k2)
type Apply (ShowListSym1 arg6989586621680260541 :: TyFun Symbol Symbol -> Type) (arg6989586621680260542 :: Symbol) Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

type Apply (ShowListSym1 arg6989586621680260541 :: TyFun Symbol Symbol -> Type) (arg6989586621680260542 :: Symbol) = ShowList arg6989586621680260541 arg6989586621680260542
type Apply (ShowsSym1 a6989586621680260525 :: TyFun Symbol Symbol -> Type) (a6989586621680260526 :: Symbol) Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

type Apply (ShowsSym1 a6989586621680260525 :: TyFun Symbol Symbol -> Type) (a6989586621680260526 :: Symbol) = Shows a6989586621680260525 a6989586621680260526
type Apply (ShowParenSym2 a6989586621680260474 a6989586621680260473 :: TyFun Symbol Symbol -> Type) (a6989586621680260475 :: Symbol) Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

type Apply (ShowParenSym2 a6989586621680260474 a6989586621680260473 :: TyFun Symbol Symbol -> Type) (a6989586621680260475 :: Symbol) = ShowParen a6989586621680260474 a6989586621680260473 a6989586621680260475
type Apply (ShowsPrecSym2 arg6989586621680260534 arg6989586621680260533 :: TyFun Symbol Symbol -> Type) (arg6989586621680260535 :: Symbol) Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

type Apply (ShowsPrecSym2 arg6989586621680260534 arg6989586621680260533 :: TyFun Symbol Symbol -> Type) (arg6989586621680260535 :: Symbol) = ShowsPrec arg6989586621680260534 arg6989586621680260533 arg6989586621680260535
type Apply (ShowListWithSym2 a6989586621680260506 a6989586621680260505 :: TyFun Symbol Symbol -> Type) (a6989586621680260507 :: Symbol) Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

type Apply (ShowListWithSym2 a6989586621680260506 a6989586621680260505 :: TyFun Symbol Symbol -> Type) (a6989586621680260507 :: Symbol) = ShowListWith a6989586621680260506 a6989586621680260505 a6989586621680260507
type Apply UnlinesSym0 (a6989586621679949055 :: [Symbol]) Source # 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

type Apply UnlinesSym0 (a6989586621679949055 :: [Symbol]) = Unlines a6989586621679949055
type Apply UnwordsSym0 (a6989586621679949044 :: [Symbol]) Source # 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

type Apply UnwordsSym0 (a6989586621679949044 :: [Symbol]) = Unwords a6989586621679949044
type Apply (FailSym0 :: TyFun Symbol (m6989586621679545990 a6989586621679545996) -> Type) (arg6989586621679546472 :: Symbol) Source # 
Instance details

Defined in Data.Singletons.Prelude.Monad.Internal

type Apply (FailSym0 :: TyFun Symbol (m6989586621679545990 a6989586621679545996) -> Type) (arg6989586621679546472 :: Symbol) = (Fail arg6989586621679546472 :: m6989586621679545990 a6989586621679545996)
type Apply ShowCharSym0 (a6989586621680260467 :: Symbol) Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

type Apply ShowCharSym0 (a6989586621680260467 :: Symbol) = ShowCharSym1 a6989586621680260467
type Apply ShowStringSym0 (a6989586621680260452 :: Symbol) Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

type Apply ShowStringSym0 (a6989586621680260452 :: Symbol) = ShowStringSym1 a6989586621680260452
type Apply ShowParenSym0 (a6989586621680260473 :: Bool) Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

type Apply ShowParenSym0 (a6989586621680260473 :: Bool) = ShowParenSym1 a6989586621680260473
type Apply (ShowsSym0 :: TyFun a6989586621680258568 (Symbol ~> Symbol) -> Type) (a6989586621680260525 :: a6989586621680258568) Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

type Apply (ShowsSym0 :: TyFun a6989586621680258568 (Symbol ~> Symbol) -> Type) (a6989586621680260525 :: a6989586621680258568) = ShowsSym1 a6989586621680260525
type Apply (ShowsPrecSym0 :: TyFun Nat (a6989586621680258583 ~> (Symbol ~> Symbol)) -> Type) (arg6989586621680260533 :: Nat) Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

type Apply (ShowsPrecSym0 :: TyFun Nat (a6989586621680258583 ~> (Symbol ~> Symbol)) -> Type) (arg6989586621680260533 :: Nat) = (ShowsPrecSym1 arg6989586621680260533 a6989586621680258583 :: TyFun a6989586621680258583 (Symbol ~> Symbol) -> Type)
type Apply (ShowsPrecSym1 arg6989586621680260533 a6989586621680258583 :: TyFun a6989586621680258583 (Symbol ~> Symbol) -> Type) (arg6989586621680260534 :: a6989586621680258583) Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

type Apply (ShowsPrecSym1 arg6989586621680260533 a6989586621680258583 :: TyFun a6989586621680258583 (Symbol ~> Symbol) -> Type) (arg6989586621680260534 :: a6989586621680258583) = ShowsPrecSym2 arg6989586621680260533 arg6989586621680260534
type Apply (ShowListSym0 :: TyFun [a6989586621680258583] (Symbol ~> Symbol) -> Type) (arg6989586621680260541 :: [a6989586621680258583]) Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

type Apply (ShowListSym0 :: TyFun [a6989586621680258583] (Symbol ~> Symbol) -> Type) (arg6989586621680260541 :: [a6989586621680258583]) = ShowListSym1 arg6989586621680260541
type Apply (ShowListWithSym1 a6989586621680260505 :: TyFun [a6989586621680258567] (Symbol ~> Symbol) -> Type) (a6989586621680260506 :: [a6989586621680258567]) Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

type Apply (ShowListWithSym1 a6989586621680260505 :: TyFun [a6989586621680258567] (Symbol ~> Symbol) -> Type) (a6989586621680260506 :: [a6989586621680258567]) = ShowListWithSym2 a6989586621680260505 a6989586621680260506
type Apply (ShowListWithSym0 :: TyFun (a6989586621680258567 ~> (Symbol ~> Symbol)) ([a6989586621680258567] ~> (Symbol ~> Symbol)) -> Type) (a6989586621680260505 :: a6989586621680258567 ~> (Symbol ~> Symbol)) Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

type Apply (ShowListWithSym0 :: TyFun (a6989586621680258567 ~> (Symbol ~> Symbol)) ([a6989586621680258567] ~> (Symbol ~> Symbol)) -> Type) (a6989586621680260505 :: a6989586621680258567 ~> (Symbol ~> Symbol)) = ShowListWithSym1 a6989586621680260505
type Apply (ShowParenSym1 a6989586621680260473 :: TyFun (Symbol ~> Symbol) (Symbol ~> Symbol) -> Type) (a6989586621680260474 :: Symbol ~> Symbol) Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

type Apply (ShowParenSym1 a6989586621680260473 :: TyFun (Symbol ~> Symbol) (Symbol ~> Symbol) -> Type) (a6989586621680260474 :: Symbol ~> Symbol) = ShowParenSym2 a6989586621680260473 a6989586621680260474

data family Sing :: k -> Type Source #

The singleton kind-indexed data family.

Instances
SDecide k => TestCoercion (Sing :: k -> Type) Source # 
Instance details

Defined in Data.Singletons.Decide

Methods

testCoercion :: Sing a -> Sing b -> Maybe (Coercion a b) Source #

SDecide k => TestEquality (Sing :: k -> Type) Source # 
Instance details

Defined in Data.Singletons.Decide

Methods

testEquality :: Sing a -> Sing b -> Maybe (a :~: b) Source #

Show (SSymbol s) Source # 
Instance details

Defined in Data.Singletons.ShowSing

Show (SNat n) Source # 
Instance details

Defined in Data.Singletons.ShowSing

Methods

showsPrec :: Int -> SNat n -> ShowS Source #

show :: SNat n -> String Source #

showList :: [SNat n] -> ShowS Source #

Eq (Sing a) Source # 
Instance details

Defined in Data.Singletons.TypeRepTYPE

Methods

(==) :: Sing a -> Sing a -> Bool Source #

(/=) :: Sing a -> Sing a -> Bool Source #

Ord (Sing a) Source # 
Instance details

Defined in Data.Singletons.TypeRepTYPE

Methods

compare :: Sing a -> Sing a -> Ordering Source #

(<) :: Sing a -> Sing a -> Bool Source #

(<=) :: Sing a -> Sing a -> Bool Source #

(>) :: Sing a -> Sing a -> Bool Source #

(>=) :: Sing a -> Sing a -> Bool Source #

max :: Sing a -> Sing a -> Sing a Source #

min :: Sing a -> Sing a -> Sing a Source #

Show (Sing z) Source # 
Instance details

Defined in Data.Singletons.ShowSing

Methods

showsPrec :: Int -> Sing z -> ShowS Source #

show :: Sing z -> String Source #

showList :: [Sing z] -> ShowS Source #

(ShowSing a, ShowSing [a]) => Show (Sing z) Source # 
Instance details

Defined in Data.Singletons.ShowSing

Methods

showsPrec :: Int -> Sing z -> ShowS Source #

show :: Sing z -> String Source #

showList :: [Sing z] -> ShowS Source #

ShowSing a => Show (Sing z) Source # 
Instance details

Defined in Data.Singletons.ShowSing

Methods

showsPrec :: Int -> Sing z -> ShowS Source #

show :: Sing z -> String Source #

showList :: [Sing z] -> ShowS Source #

Show (Sing z) Source # 
Instance details

Defined in Data.Singletons.ShowSing

Methods

showsPrec :: Int -> Sing z -> ShowS Source #

show :: Sing z -> String Source #

showList :: [Sing z] -> ShowS Source #

(ShowSing a, ShowSing b) => Show (Sing z) Source # 
Instance details

Defined in Data.Singletons.ShowSing

Methods

showsPrec :: Int -> Sing z -> ShowS Source #

show :: Sing z -> String Source #

showList :: [Sing z] -> ShowS Source #

Show (Sing a) Source # 
Instance details

Defined in Data.Singletons.TypeRepTYPE

Methods

showsPrec :: Int -> Sing a -> ShowS Source #

show :: Sing a -> String Source #

showList :: [Sing a] -> ShowS Source #

Show (Sing z) Source # 
Instance details

Defined in Data.Singletons.ShowSing

Methods

showsPrec :: Int -> Sing z -> ShowS Source #

show :: Sing z -> String Source #

showList :: [Sing z] -> ShowS Source #

(ShowSing a, ShowSing b) => Show (Sing z) Source # 
Instance details

Defined in Data.Singletons.ShowSing

Methods

showsPrec :: Int -> Sing z -> ShowS Source #

show :: Sing z -> String Source #

showList :: [Sing z] -> ShowS Source #

(ShowSing a, ShowSing b, ShowSing c) => Show (Sing z) Source # 
Instance details

Defined in Data.Singletons.ShowSing

Methods

showsPrec :: Int -> Sing z -> ShowS Source #

show :: Sing z -> String Source #

showList :: [Sing z] -> ShowS Source #

(ShowSing a, ShowSing b, ShowSing c, ShowSing d) => Show (Sing z) Source # 
Instance details

Defined in Data.Singletons.ShowSing

Methods

showsPrec :: Int -> Sing z -> ShowS Source #

show :: Sing z -> String Source #

showList :: [Sing z] -> ShowS Source #

(ShowSing a, ShowSing b, ShowSing c, ShowSing d, ShowSing e) => Show (Sing z) Source # 
Instance details

Defined in Data.Singletons.ShowSing

Methods

showsPrec :: Int -> Sing z -> ShowS Source #

show :: Sing z -> String Source #

showList :: [Sing z] -> ShowS Source #

(ShowSing a, ShowSing b, ShowSing c, ShowSing d, ShowSing e, ShowSing f) => Show (Sing z) Source # 
Instance details

Defined in Data.Singletons.ShowSing

Methods

showsPrec :: Int -> Sing z -> ShowS Source #

show :: Sing z -> String Source #

showList :: [Sing z] -> ShowS Source #

(ShowSing a, ShowSing b, ShowSing c, ShowSing d, ShowSing e, ShowSing f, ShowSing g) => Show (Sing z) Source # 
Instance details

Defined in Data.Singletons.ShowSing

Methods

showsPrec :: Int -> Sing z -> ShowS Source #

show :: Sing z -> String Source #

showList :: [Sing z] -> ShowS Source #

Show (Sing z) Source # 
Instance details

Defined in Data.Singletons.ShowSing

Methods

showsPrec :: Int -> Sing z -> ShowS Source #

show :: Sing z -> String Source #

showList :: [Sing z] -> ShowS Source #

ShowSing a => Show (Sing z) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup

Methods

showsPrec :: Int -> Sing z -> ShowS Source #

show :: Sing z -> String Source #

showList :: [Sing z] -> ShowS Source #

ShowSing a => Show (Sing z) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup

Methods

showsPrec :: Int -> Sing z -> ShowS Source #

show :: Sing z -> String Source #

showList :: [Sing z] -> ShowS Source #

(ShowSing a, ShowSing b) => Show (Sing z) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup

Methods

showsPrec :: Int -> Sing z -> ShowS Source #

show :: Sing z -> String Source #

showList :: [Sing z] -> ShowS Source #

ShowSing a => Show (Sing z) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup

Methods

showsPrec :: Int -> Sing z -> ShowS Source #

show :: Sing z -> String Source #

showList :: [Sing z] -> ShowS Source #

ShowSing a => Show (Sing z) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup

Methods

showsPrec :: Int -> Sing z -> ShowS Source #

show :: Sing z -> String Source #

showList :: [Sing z] -> ShowS Source #

ShowSing m => Show (Sing z) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup

Methods

showsPrec :: Int -> Sing z -> ShowS Source #

show :: Sing z -> String Source #

showList :: [Sing z] -> ShowS Source #

ShowSing (Maybe a) => Show (Sing z) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup

Methods

showsPrec :: Int -> Sing z -> ShowS Source #

show :: Sing z -> String Source #

showList :: [Sing z] -> ShowS Source #

ShowSing a => Show (Sing z) Source # 
Instance details

Defined in Data.Singletons.ShowSing

Methods

showsPrec :: Int -> Sing z -> ShowS Source #

show :: Sing z -> String Source #

showList :: [Sing z] -> ShowS Source #

ShowSing (Maybe a) => Show (Sing z) Source # 
Instance details

Defined in Data.Singletons.Prelude.Monoid

Methods

showsPrec :: Int -> Sing z -> ShowS Source #

show :: Sing z -> String Source #

showList :: [Sing z] -> ShowS Source #

ShowSing (Maybe a) => Show (Sing z) Source # 
Instance details

Defined in Data.Singletons.Prelude.Monoid

Methods

showsPrec :: Int -> Sing z -> ShowS Source #

show :: Sing z -> String Source #

showList :: [Sing z] -> ShowS Source #

ShowSing a => Show (Sing z) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup

Methods

showsPrec :: Int -> Sing z -> ShowS Source #

show :: Sing z -> String Source #

showList :: [Sing z] -> ShowS Source #

ShowSing Bool => Show (Sing z) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup

Methods

showsPrec :: Int -> Sing z -> ShowS Source #

show :: Sing z -> String Source #

showList :: [Sing z] -> ShowS Source #

ShowSing Bool => Show (Sing z) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup

Methods

showsPrec :: Int -> Sing z -> ShowS Source #

show :: Sing z -> String Source #

showList :: [Sing z] -> ShowS Source #

ShowSing a => Show (Sing z) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup

Methods

showsPrec :: Int -> Sing z -> ShowS Source #

show :: Sing z -> String Source #

showList :: [Sing z] -> ShowS Source #

ShowSing a => Show (Sing z) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup

Methods

showsPrec :: Int -> Sing z -> ShowS Source #

show :: Sing z -> String Source #

showList :: [Sing z] -> ShowS Source #

(ShowSing a, ShowSing [a]) => Show (Sing z) Source # 
Instance details

Defined in Data.Singletons.ShowSing

Methods

showsPrec :: Int -> Sing z -> ShowS Source #

show :: Sing z -> String Source #

showList :: [Sing z] -> ShowS Source #

data Sing (a :: Bool) Source # 
Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (a :: Bool) where
data Sing (a :: Ordering) Source # 
Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (a :: Ordering) where
data Sing (n :: Nat) Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

data Sing (n :: Nat) where
data Sing (n :: Symbol) Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

data Sing (n :: Symbol) where
data Sing (a :: ()) Source # 
Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (a :: ()) where
data Sing (a :: Void) Source # 
Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (a :: Void)
data Sing (a :: All) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (a :: All) where
data Sing (a :: Any) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (a :: Any) where
data Sing (a :: PErrorMessage) Source # 
Instance details

Defined in Data.Singletons.TypeError

data Sing (a :: PErrorMessage) where
data Sing (b :: [a]) Source # 
Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (b :: [a]) where
  • SNil :: forall k (b :: [k]). Sing ([] :: [k])
  • SCons :: forall a (b :: [a]) (n :: a) (n :: [a]). Sing n -> Sing n -> Sing (n ': n)
data Sing (b :: Maybe a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (b :: Maybe a) where
newtype Sing (a :: TYPE rep) Source #

A choice of singleton for the kind TYPE rep (for some RuntimeRep rep), an instantiation of which is the famous kind Type.

Conceivably, one could generalize this instance to `Sing :: k -> Type` for any kind k, and remove all other Sing instances. We don't adopt this design, however, since it is far more convenient in practice to work with explicit singleton values than TypeReps (for instance, TypeReps are more difficult to pattern match on, and require extra runtime checks).

We cannot produce explicit singleton values for everything in TYPE rep, however, since it is an open kind, so we reach for TypeRep in this one particular case.

Instance details

Defined in Data.Singletons.TypeRepTYPE

newtype Sing (a :: TYPE rep) = STypeRep (TypeRep a)
data Sing (b :: Min a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: Min a) where
data Sing (b :: Max a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: Max a) where
data Sing (b :: First a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: First a) where
data Sing (b :: Last a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: Last a) where
data Sing (a :: WrappedMonoid m) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (a :: WrappedMonoid m) where
data Sing (b :: Option a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: Option a) where
data Sing (b :: Identity a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (b :: Identity a) where
data Sing (b :: First a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Monoid

data Sing (b :: First a) where
data Sing (b :: Last a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Monoid

data Sing (b :: Last a) where
data Sing (b :: Dual a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: Dual a) where
data Sing (b :: Sum a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: Sum a) where
data Sing (b :: Product a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: Product a) where
data Sing (b :: Down a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Ord

data Sing (b :: Down a) where
data Sing (b :: NonEmpty a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (b :: NonEmpty a) where
data Sing (c :: Either a b) Source # 
Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (c :: Either a b) where
data Sing (c :: (a, b)) Source # 
Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (c :: (a, b)) where
data Sing (c :: Arg a b) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup

data Sing (c :: Arg a b) where
newtype Sing (f :: k1 ~> k2) Source # 
Instance details

Defined in Data.Singletons.Internal

newtype Sing (f :: k1 ~> k2) = SLambda {}
data Sing (d :: (a, b, c)) Source # 
Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (d :: (a, b, c)) where
data Sing (c :: Const a b) Source # 
Instance details

Defined in Data.Singletons.Prelude.Const

data Sing (c :: Const a b) where
data Sing (e :: (a, b, c, d)) Source # 
Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (e :: (a, b, c, d)) where
data Sing (f :: (a, b, c, d, e)) Source # 
Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (f :: (a, b, c, d, e)) where
data Sing (g :: (a, b, c, d, e, f)) Source # 
Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (g :: (a, b, c, d, e, f)) where
data Sing (h :: (a, b, c, d, e, f, g)) Source # 
Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (h :: (a, b, c, d, e, f, g)) where

type SNat (x :: Nat) = Sing x Source #

Kind-restricted synonym for Sing for Nats

type SSymbol (x :: Symbol) = Sing x Source #

Kind-restricted synonym for Sing for Symbols

withKnownNat :: Sing n -> (KnownNat n => r) -> r Source #

Given a singleton for Nat, call something requiring a KnownNat instance.

withKnownSymbol :: Sing n -> (KnownSymbol n => r) -> r Source #

Given a singleton for Symbol, call something requiring a KnownSymbol instance.

type family Error (str :: k0) :: k where ... Source #

The promotion of error. This version is more poly-kinded for easier use.

sError :: HasCallStack => Sing (str :: Symbol) -> a Source #

The singleton for error

type family ErrorWithoutStackTrace (str :: k0) :: k where ... Source #

The promotion of errorWithoutStackTrace. This version is more poly-kinded for easier use.

type family Undefined :: k where ... Source #

The promotion of undefined.

sUndefined :: HasCallStack => a Source #

The singleton for undefined.

class KnownNat (n :: Nat) Source #

This class gives the integer associated with a type-level natural. There are instances of the class for every concrete literal: 0, 1, 2, etc.

Since: base-4.7.0.0

Minimal complete definition

natSing

natVal :: KnownNat n => proxy n -> Natural Source #

Since: base-4.10.0.0

class KnownSymbol (n :: Symbol) Source #

This class gives the string associated with a type-level symbol. There are instances of the class for every concrete literal: "hello", etc.

Since: base-4.7.0.0

Minimal complete definition

symbolSing

symbolVal :: KnownSymbol n => proxy n -> String Source #

Since: base-4.7.0.0

type family (a :: Nat) ^ (b :: Nat) :: Nat where ... infixr 8 Source #

Exponentiation of type-level naturals.

Since: base-4.7.0.0

(%^) :: Sing a -> Sing b -> Sing (a ^ b) infixr 8 Source #

The singleton analogue of '(TN.^)' for Nats.

type family (a :: Nat) <=? (b :: Nat) :: Bool where ... infix 4 Source #

Comparison of type-level naturals, as a function. NOTE: The functionality for this function should be subsumed by CmpNat, so this might go away in the future. Please let us know, if you encounter discrepancies between the two.

(%<=?) :: Sing a -> Sing b -> Sing (a <=? b) infix 4 Source #

The singleton analogue of <=?

Note that, because of historical reasons in GHC's Nat API, <=? is incompatible (unification-wise) with <= and the PEq, SEq, POrd, and SOrd instances for Nat. (a <=? b) ~ 'True does not imply anything about a <= b or any other PEq / POrd relationships.

(Be aware that <= in the paragraph above refers to <= from the POrd typeclass, exported from Data.Singletons.Prelude.Ord, and not the <= from GHC.TypeNats. The latter is simply a type alias for (a <=? b) ~ 'True.)

This is provided here for the sake of completeness and for compatibility with libraries with APIs built around <=?. New code should use CmpNat, exposed through this library through the POrd and SOrd instances for Nat.

type family Log2 (a :: Nat) :: Nat where ... Source #

Log base 2 (round down) of natural numbers. Log 0 is undefined (i.e., it cannot be reduced).

Since: base-4.11.0.0

sLog2 :: Sing x -> Sing (Log2 x) Source #

type family Div (a :: Nat) (b :: Nat) :: Nat where ... infixl 7 Source #

Division (round down) of natural numbers. Div x 0 is undefined (i.e., it cannot be reduced).

Since: base-4.11.0.0

sDiv :: Sing x -> Sing y -> Sing (Div x y) infixl 7 Source #

type family Mod (a :: Nat) (b :: Nat) :: Nat where ... infixl 7 Source #

Modulus of natural numbers. Mod x 0 is undefined (i.e., it cannot be reduced).

Since: base-4.11.0.0

sMod :: Sing x -> Sing y -> Sing (Mod x y) infixl 7 Source #

type family DivMod (a :: Nat) (a :: Nat) :: (Nat, Nat) where ... Source #

Equations

DivMod x y = Apply (Apply Tuple2Sym0 (Apply (Apply DivSym0 x) y)) (Apply (Apply ModSym0 x) y) 

sDivMod :: Sing x -> Sing y -> Sing (DivMod x y) Source #

type family Quot (a :: Nat) (a :: Nat) :: Nat where ... infixl 7 Source #

Equations

Quot a_6989586621679488496 a_6989586621679488498 = Apply (Apply DivSym0 a_6989586621679488496) a_6989586621679488498 

sQuot :: Sing x -> Sing y -> Sing (Quot x y) infixl 7 Source #

type family Rem (a :: Nat) (a :: Nat) :: Nat where ... infixl 7 Source #

Equations

Rem a_6989586621679488486 a_6989586621679488488 = Apply (Apply ModSym0 a_6989586621679488486) a_6989586621679488488 

sRem :: Sing x -> Sing y -> Sing (Rem x y) infixl 7 Source #

type family QuotRem (a :: Nat) (a :: Nat) :: (Nat, Nat) where ... Source #

Equations

QuotRem a_6989586621679488512 a_6989586621679488514 = Apply (Apply DivModSym0 a_6989586621679488512) a_6989586621679488514 

sQuotRem :: Sing x -> Sing y -> Sing (QuotRem x y) Source #

Defunctionalization symbols

data ErrorSym0 :: forall k06989586621679468915 k6989586621679468914. (~>) k06989586621679468915 k6989586621679468914 Source #

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

Defined in Data.Singletons.TypeLits.Internal

SuppressUnusedWarnings (ErrorSym0 :: TyFun k06989586621679468915 k6989586621679468914 -> Type) Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

type Apply (ErrorSym0 :: TyFun k0 k2 -> Type) (str6989586621679468916 :: k0) Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

type Apply (ErrorSym0 :: TyFun k0 k2 -> Type) (str6989586621679468916 :: k0) = (Error str6989586621679468916 :: k2)

type ErrorSym1 (str6989586621679468916 :: k06989586621679468915) = Error str6989586621679468916 Source #

data ErrorWithoutStackTraceSym0 :: forall k06989586621679469965 k6989586621679469964. (~>) k06989586621679469965 k6989586621679469964 Source #

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

Defined in Data.Singletons.TypeLits.Internal

SuppressUnusedWarnings (ErrorWithoutStackTraceSym0 :: TyFun k06989586621679469965 k6989586621679469964 -> Type) Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

type Apply (ErrorWithoutStackTraceSym0 :: TyFun k0 k2 -> Type) (str6989586621679469966 :: k0) Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

type Apply (ErrorWithoutStackTraceSym0 :: TyFun k0 k2 -> Type) (str6989586621679469966 :: k0) = (ErrorWithoutStackTrace str6989586621679469966 :: k2)

type ErrorWithoutStackTraceSym1 (str6989586621679469966 :: k06989586621679469965) = ErrorWithoutStackTrace str6989586621679469966 Source #

data KnownNatSym0 :: (~>) Nat Constraint Source #

Instances
SuppressUnusedWarnings KnownNatSym0 Source # 
Instance details

Defined in Data.Singletons.TypeLits

type Apply KnownNatSym0 (n6989586621679469170 :: Nat) Source # 
Instance details

Defined in Data.Singletons.TypeLits

type Apply KnownNatSym0 (n6989586621679469170 :: Nat) = KnownNat n6989586621679469170

type KnownNatSym1 (n6989586621679469170 :: Nat) = KnownNat n6989586621679469170 Source #

data KnownSymbolSym0 :: (~>) Symbol Constraint Source #

Instances
SuppressUnusedWarnings KnownSymbolSym0 Source # 
Instance details

Defined in Data.Singletons.TypeLits

type Apply KnownSymbolSym0 (n6989586621679469110 :: Symbol) Source # 
Instance details

Defined in Data.Singletons.TypeLits

type Apply KnownSymbolSym0 (n6989586621679469110 :: Symbol) = KnownSymbol n6989586621679469110

type KnownSymbolSym1 (n6989586621679469110 :: Symbol) = KnownSymbol n6989586621679469110 Source #

data (^@#@$) :: (~>) Nat ((~>) Nat Nat) infixr 8 Source #

Instances
SingI (^@#@$) Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

SuppressUnusedWarnings (^@#@$) Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

type Apply (^@#@$) (a3530822107858468865 :: Nat) Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

type Apply (^@#@$) (a3530822107858468865 :: Nat) = (^@#@$$) a3530822107858468865

data (^@#@$$) (a3530822107858468865 :: Nat) :: (~>) Nat Nat infixr 8 Source #

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

Defined in Data.Singletons.TypeLits.Internal

Methods

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

SuppressUnusedWarnings ((^@#@$$) a3530822107858468865 :: TyFun Nat Nat -> Type) Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

type Apply ((^@#@$$) a3530822107858468865 :: TyFun Nat Nat -> Type) (b3530822107858468866 :: Nat) Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

type Apply ((^@#@$$) a3530822107858468865 :: TyFun Nat Nat -> Type) (b3530822107858468866 :: Nat) = a3530822107858468865 ^ b3530822107858468866

type (^@#@$$$) (a3530822107858468865 :: Nat) (b3530822107858468866 :: Nat) = (^) a3530822107858468865 b3530822107858468866 Source #

data (<=?@#@$) :: (~>) Nat ((~>) Nat Bool) infix 4 Source #

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

Defined in Data.Singletons.TypeLits.Internal

SuppressUnusedWarnings (<=?@#@$) Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

type Apply (<=?@#@$) (a3530822107858468865 :: Nat) Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

type Apply (<=?@#@$) (a3530822107858468865 :: Nat) = (<=?@#@$$) a3530822107858468865

data (<=?@#@$$) (a3530822107858468865 :: Nat) :: (~>) Nat Bool infix 4 Source #

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

Defined in Data.Singletons.TypeLits.Internal

Methods

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

SuppressUnusedWarnings ((<=?@#@$$) a3530822107858468865 :: TyFun Nat Bool -> Type) Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

type Apply ((<=?@#@$$) a3530822107858468865 :: TyFun Nat Bool -> Type) (b3530822107858468866 :: Nat) Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

type Apply ((<=?@#@$$) a3530822107858468865 :: TyFun Nat Bool -> Type) (b3530822107858468866 :: Nat) = a3530822107858468865 <=? b3530822107858468866

type (<=?@#@$$$) (a3530822107858468865 :: Nat) (b3530822107858468866 :: Nat) = (<=?) a3530822107858468865 b3530822107858468866 Source #

data Log2Sym0 :: (~>) Nat Nat Source #

Instances
SingI Log2Sym0 Source # 
Instance details

Defined in Data.Singletons.TypeLits

SuppressUnusedWarnings Log2Sym0 Source # 
Instance details

Defined in Data.Singletons.TypeLits

type Apply Log2Sym0 (a3530822107858468865 :: Nat) Source # 
Instance details

Defined in Data.Singletons.TypeLits

type Apply Log2Sym0 (a3530822107858468865 :: Nat) = Log2 a3530822107858468865

type Log2Sym1 (a3530822107858468865 :: Nat) = Log2 a3530822107858468865 Source #

data DivSym0 :: (~>) Nat ((~>) Nat Nat) infixl 7 Source #

Instances
SingI DivSym0 Source # 
Instance details

Defined in Data.Singletons.TypeLits

SuppressUnusedWarnings DivSym0 Source # 
Instance details

Defined in Data.Singletons.TypeLits

type Apply DivSym0 (a3530822107858468865 :: Nat) Source # 
Instance details

Defined in Data.Singletons.TypeLits

type Apply DivSym0 (a3530822107858468865 :: Nat) = DivSym1 a3530822107858468865

data DivSym1 (a3530822107858468865 :: Nat) :: (~>) Nat Nat infixl 7 Source #

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

Defined in Data.Singletons.TypeLits

Methods

sing :: Sing (DivSym1 x) Source #

SuppressUnusedWarnings (DivSym1 a3530822107858468865 :: TyFun Nat Nat -> Type) Source # 
Instance details

Defined in Data.Singletons.TypeLits

type Apply (DivSym1 a3530822107858468865 :: TyFun Nat Nat -> Type) (b3530822107858468866 :: Nat) Source # 
Instance details

Defined in Data.Singletons.TypeLits

type Apply (DivSym1 a3530822107858468865 :: TyFun Nat Nat -> Type) (b3530822107858468866 :: Nat) = Div a3530822107858468865 b3530822107858468866

type DivSym2 (a3530822107858468865 :: Nat) (b3530822107858468866 :: Nat) = Div a3530822107858468865 b3530822107858468866 Source #

data ModSym0 :: (~>) Nat ((~>) Nat Nat) infixl 7 Source #

Instances
SingI ModSym0 Source # 
Instance details

Defined in Data.Singletons.TypeLits

SuppressUnusedWarnings ModSym0 Source # 
Instance details

Defined in Data.Singletons.TypeLits

type Apply ModSym0 (a3530822107858468865 :: Nat) Source # 
Instance details

Defined in Data.Singletons.TypeLits

type Apply ModSym0 (a3530822107858468865 :: Nat) = ModSym1 a3530822107858468865

data ModSym1 (a3530822107858468865 :: Nat) :: (~>) Nat Nat infixl 7 Source #

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

Defined in Data.Singletons.TypeLits

Methods

sing :: Sing (ModSym1 x) Source #

SuppressUnusedWarnings (ModSym1 a3530822107858468865 :: TyFun Nat Nat -> Type) Source # 
Instance details

Defined in Data.Singletons.TypeLits

type Apply (ModSym1 a3530822107858468865 :: TyFun Nat Nat -> Type) (b3530822107858468866 :: Nat) Source # 
Instance details

Defined in Data.Singletons.TypeLits

type Apply (ModSym1 a3530822107858468865 :: TyFun Nat Nat -> Type) (b3530822107858468866 :: Nat) = Mod a3530822107858468865 b3530822107858468866

type ModSym2 (a3530822107858468865 :: Nat) (b3530822107858468866 :: Nat) = Mod a3530822107858468865 b3530822107858468866 Source #

data DivModSym0 :: (~>) Nat ((~>) Nat (Nat, Nat)) Source #

Instances
SuppressUnusedWarnings DivModSym0 Source # 
Instance details

Defined in Data.Singletons.TypeLits

type Apply DivModSym0 (a6989586621679488506 :: Nat) Source # 
Instance details

Defined in Data.Singletons.TypeLits

type Apply DivModSym0 (a6989586621679488506 :: Nat) = DivModSym1 a6989586621679488506

data DivModSym1 (a6989586621679488506 :: Nat) :: (~>) Nat (Nat, Nat) Source #

Instances
SuppressUnusedWarnings (DivModSym1 a6989586621679488506 :: TyFun Nat (Nat, Nat) -> Type) Source # 
Instance details

Defined in Data.Singletons.TypeLits

type Apply (DivModSym1 a6989586621679488506 :: TyFun Nat (Nat, Nat) -> Type) (a6989586621679488507 :: Nat) Source # 
Instance details

Defined in Data.Singletons.TypeLits

type Apply (DivModSym1 a6989586621679488506 :: TyFun Nat (Nat, Nat) -> Type) (a6989586621679488507 :: Nat) = DivMod a6989586621679488506 a6989586621679488507

type DivModSym2 (a6989586621679488506 :: Nat) (a6989586621679488507 :: Nat) = DivMod a6989586621679488506 a6989586621679488507 Source #

data QuotSym0 :: (~>) Nat ((~>) Nat Nat) infixl 7 Source #

Instances
SuppressUnusedWarnings QuotSym0 Source # 
Instance details

Defined in Data.Singletons.TypeLits

type Apply QuotSym0 (a6989586621679488500 :: Nat) Source # 
Instance details

Defined in Data.Singletons.TypeLits

type Apply QuotSym0 (a6989586621679488500 :: Nat) = QuotSym1 a6989586621679488500

data QuotSym1 (a6989586621679488500 :: Nat) :: (~>) Nat Nat infixl 7 Source #

Instances
SuppressUnusedWarnings (QuotSym1 a6989586621679488500 :: TyFun Nat Nat -> Type) Source # 
Instance details

Defined in Data.Singletons.TypeLits

type Apply (QuotSym1 a6989586621679488500 :: TyFun Nat Nat -> Type) (a6989586621679488501 :: Nat) Source # 
Instance details

Defined in Data.Singletons.TypeLits

type Apply (QuotSym1 a6989586621679488500 :: TyFun Nat Nat -> Type) (a6989586621679488501 :: Nat) = Quot a6989586621679488500 a6989586621679488501

type QuotSym2 (a6989586621679488500 :: Nat) (a6989586621679488501 :: Nat) = Quot a6989586621679488500 a6989586621679488501 Source #

data RemSym0 :: (~>) Nat ((~>) Nat Nat) infixl 7 Source #

Instances
SuppressUnusedWarnings RemSym0 Source # 
Instance details

Defined in Data.Singletons.TypeLits

type Apply RemSym0 (a6989586621679488490 :: Nat) Source # 
Instance details

Defined in Data.Singletons.TypeLits

type Apply RemSym0 (a6989586621679488490 :: Nat) = RemSym1 a6989586621679488490

data RemSym1 (a6989586621679488490 :: Nat) :: (~>) Nat Nat infixl 7 Source #

Instances
SuppressUnusedWarnings (RemSym1 a6989586621679488490 :: TyFun Nat Nat -> Type) Source # 
Instance details

Defined in Data.Singletons.TypeLits

type Apply (RemSym1 a6989586621679488490 :: TyFun Nat Nat -> Type) (a6989586621679488491 :: Nat) Source # 
Instance details

Defined in Data.Singletons.TypeLits

type Apply (RemSym1 a6989586621679488490 :: TyFun Nat Nat -> Type) (a6989586621679488491 :: Nat) = Rem a6989586621679488490 a6989586621679488491

type RemSym2 (a6989586621679488490 :: Nat) (a6989586621679488491 :: Nat) = Rem a6989586621679488490 a6989586621679488491 Source #

data QuotRemSym0 :: (~>) Nat ((~>) Nat (Nat, Nat)) Source #

Instances
SuppressUnusedWarnings QuotRemSym0 Source # 
Instance details

Defined in Data.Singletons.TypeLits

type Apply QuotRemSym0 (a6989586621679488516 :: Nat) Source # 
Instance details

Defined in Data.Singletons.TypeLits

type Apply QuotRemSym0 (a6989586621679488516 :: Nat) = QuotRemSym1 a6989586621679488516

data QuotRemSym1 (a6989586621679488516 :: Nat) :: (~>) Nat (Nat, Nat) Source #

Instances
SuppressUnusedWarnings (QuotRemSym1 a6989586621679488516 :: TyFun Nat (Nat, Nat) -> Type) Source # 
Instance details

Defined in Data.Singletons.TypeLits

type Apply (QuotRemSym1 a6989586621679488516 :: TyFun Nat (Nat, Nat) -> Type) (a6989586621679488517 :: Nat) Source # 
Instance details

Defined in Data.Singletons.TypeLits

type Apply (QuotRemSym1 a6989586621679488516 :: TyFun Nat (Nat, Nat) -> Type) (a6989586621679488517 :: Nat) = QuotRem a6989586621679488516 a6989586621679488517

type QuotRemSym2 (a6989586621679488516 :: Nat) (a6989586621679488517 :: Nat) = QuotRem a6989586621679488516 a6989586621679488517 Source #

Orphan instances

Enum Nat Source # 
Instance details

Eq Nat Source # 
Instance details

Methods

(==) :: Nat -> Nat -> Bool Source #

(/=) :: Nat -> Nat -> Bool Source #

Eq Symbol Source #

This bogus instance is helpful for people who want to define functions over Symbols that will only be used at the type level or as singletons.

Instance details

Num Nat Source #

This bogus Num instance is helpful for people who want to define functions over Nats that will only be used at the type level or as singletons. A correct SNum instance for Nat singletons exists.

Instance details

Ord Nat Source # 
Instance details

Methods

compare :: Nat -> Nat -> Ordering Source #

(<) :: Nat -> Nat -> Bool Source #

(<=) :: Nat -> Nat -> Bool Source #

(>) :: Nat -> Nat -> Bool Source #

(>=) :: Nat -> Nat -> Bool Source #

max :: Nat -> Nat -> Nat Source #

min :: Nat -> Nat -> Nat Source #

Ord Symbol Source # 
Instance details

Show Nat Source # 
Instance details

Show Symbol Source # 
Instance details

IsString Symbol Source # 
Instance details

Semigroup Symbol Source # 
Instance details

Monoid Symbol Source # 
Instance details