Data.Singletons.TypeLits

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

Documentation

data Nat

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

Instances

Enum Nat

Defined in Data.Singletons.TypeLits

Methods

succ :: Nat -> Nat

pred :: Nat -> Nat

toEnum :: Int -> Nat

fromEnum :: Nat -> Int

enumFrom :: Nat -> [Nat]

enumFromThen :: Nat -> Nat -> [Nat]

enumFromTo :: Nat -> Nat -> [Nat]

enumFromThenTo :: Nat -> Nat -> Nat -> [Nat]

Eq Nat

Defined in Data.Singletons.TypeLits

Methods

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

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

Num Nat

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.

Defined in Data.Singletons.TypeLits

Methods

(+) :: Nat -> Nat -> Nat

(-) :: Nat -> Nat -> Nat

(*) :: Nat -> Nat -> Nat

negate :: Nat -> Nat

abs :: Nat -> Nat

signum :: Nat -> Nat

fromInteger :: Integer -> Nat

Ord Nat

Defined in Data.Singletons.TypeLits

Methods

compare :: Nat -> Nat -> Ordering

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

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

(>) :: Nat -> Nat -> Bool

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

max :: Nat -> Nat -> Nat

min :: Nat -> Nat -> Nat

Show Nat

Defined in Data.Singletons.TypeLits

Methods

showsPrec :: Int -> Nat -> ShowS

show :: Nat -> String

showList :: [Nat] -> ShowS

SingKind Nat

Defined in Data.Singletons.TypeLits.Internal

Associated Types

type Demote Nat = (r :: Type)

Methods

fromSing :: Sing a -> Demote Nat

toSing :: Demote Nat -> SomeSing Nat

SDecide Nat

Defined in Data.Singletons.TypeLits.Internal

Methods

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

PEq Nat

Defined in Data.Singletons.TypeLits.Internal

Associated Types

type x == y :: Bool

type x /= y :: Bool

SEq Nat

Defined in Data.Singletons.TypeLits.Internal

Methods

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

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

SOrd Nat

Defined in Data.Singletons.TypeLits.Internal

Methods

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

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

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

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

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

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

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

POrd Nat

Defined in Data.Singletons.TypeLits.Internal

Associated Types

type Compare arg arg :: Ordering

type arg < arg :: Bool

type arg <= arg :: Bool

type arg > arg :: Bool

type arg >= arg :: Bool

type Max arg arg :: a

type Min arg arg :: a

SNum Nat

Defined in Data.Singletons.Prelude.Num

Methods

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

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

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

sNegate :: Sing t -> Sing (Apply NegateSym0 t)

sAbs :: Sing t -> Sing (Apply AbsSym0 t)

sSignum :: Sing t -> Sing (Apply SignumSym0 t)

sFromInteger :: Sing t -> Sing (Apply FromIntegerSym0 t)

PNum Nat

Defined in Data.Singletons.Prelude.Num

Associated Types

type arg + arg :: a

type arg - arg :: a

type arg * arg :: a

type Negate arg :: a

type Abs arg :: a

type Signum arg :: a

type FromInteger arg :: a

SEnum Nat

Defined in Data.Singletons.Prelude.Enum

Methods

sSucc :: Sing t -> Sing (Apply SuccSym0 t)

sPred :: Sing t -> Sing (Apply PredSym0 t)

sToEnum :: Sing t -> Sing (Apply ToEnumSym0 t)

sFromEnum :: Sing t -> Sing (Apply FromEnumSym0 t)

sEnumFromTo :: Sing t -> Sing t -> Sing (Apply (Apply EnumFromToSym0 t) t)

sEnumFromThenTo :: Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply EnumFromThenToSym0 t) t) t)

PEnum Nat

Defined in Data.Singletons.Prelude.Enum

Associated Types

type Succ arg :: a

type Pred arg :: a

type ToEnum arg :: a

type FromEnum arg :: Nat

type EnumFromTo arg arg :: [a]

type EnumFromThenTo arg arg arg :: [a]

SShow Nat

Defined in Data.Singletons.Prelude.Show

Methods

sShowsPrec :: Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply ShowsPrecSym0 t) t) t)

sShow_ :: Sing t -> Sing (Apply Show_Sym0 t)

sShowList :: Sing t -> Sing t -> Sing (Apply (Apply ShowListSym0 t) t)

PShow Nat

Defined in Data.Singletons.Prelude.Show

Associated Types

type ShowsPrec arg arg arg :: Symbol

type Show_ arg :: Symbol

type ShowList arg arg :: Symbol

KnownNat n => SingI (n :: Nat)

Defined in Data.Singletons.TypeLits.Internal

Methods

sing :: Sing n

Show (SNat n)

Defined in Data.Singletons.ShowSing

Methods

showsPrec :: Int -> SNat n -> ShowS

show :: SNat n -> String

showList :: [SNat n] -> ShowS

SingI Log2Sym0

Defined in Data.Singletons.TypeLits

Methods

sing :: Sing Log2Sym0

SingI (<=?@#@$)

Defined in Data.Singletons.TypeLits.Internal

Methods

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

SingI (^@#@$)

Defined in Data.Singletons.TypeLits.Internal

Methods

sing :: Sing (^@#@$)

SingI DivSym0

Defined in Data.Singletons.TypeLits

Methods

sing :: Sing DivSym0

SingI ModSym0

Defined in Data.Singletons.TypeLits

Methods

sing :: Sing ModSym0

SuppressUnusedWarnings KnownNatSym0

Defined in Data.Singletons.TypeLits

Methods

suppressUnusedWarnings :: ()

SuppressUnusedWarnings Log2Sym0

Defined in Data.Singletons.TypeLits

Methods

suppressUnusedWarnings :: ()

SuppressUnusedWarnings (<=?@#@$)

Defined in Data.Singletons.TypeLits.Internal

Methods

suppressUnusedWarnings :: ()

SuppressUnusedWarnings (^@#@$)

Defined in Data.Singletons.TypeLits.Internal

Methods

suppressUnusedWarnings :: ()

SuppressUnusedWarnings DivSym0

Defined in Data.Singletons.TypeLits

Methods

suppressUnusedWarnings :: ()

SuppressUnusedWarnings ModSym0

Defined in Data.Singletons.TypeLits

Methods

suppressUnusedWarnings :: ()

SuppressUnusedWarnings QuotSym0

Defined in Data.Singletons.TypeLits

Methods

suppressUnusedWarnings :: ()

SuppressUnusedWarnings RemSym0

Defined in Data.Singletons.TypeLits

Methods

suppressUnusedWarnings :: ()

SuppressUnusedWarnings QuotRemSym0

Defined in Data.Singletons.TypeLits

Methods

suppressUnusedWarnings :: ()

SuppressUnusedWarnings DivModSym0

Defined in Data.Singletons.TypeLits

Methods

suppressUnusedWarnings :: ()

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

Defined in Data.Singletons.TypeLits.Internal

Methods

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

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

Defined in Data.Singletons.TypeLits.Internal

Methods

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

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

Defined in Data.Singletons.TypeLits

Methods

sing :: Sing (DivSym1 x)

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

Defined in Data.Singletons.TypeLits

Methods

sing :: Sing (ModSym1 x)

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

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

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

Defined in Data.Singletons.Prelude.Num

Methods

sing :: Sing FromIntegerSym0

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

Defined in Data.Singletons.Prelude.Enum

Methods

sing :: Sing ToEnumSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing SplitAtSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing DropSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing TakeSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing ReplicateSym0

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

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing ShowsPrecSym0

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

Defined in Data.Singletons.Prelude.List.NonEmpty

Methods

sing :: Sing SplitAtSym0

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

Defined in Data.Singletons.Prelude.List.NonEmpty

Methods

sing :: Sing DropSym0

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

Defined in Data.Singletons.Prelude.List.NonEmpty

Methods

sing :: Sing TakeSym0

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

Defined in Data.Singletons.Prelude.Enum

Methods

sing :: Sing FromEnumSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing ElemIndicesSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing ElemIndexSym0

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

Defined in Data.Singletons.Prelude.List.NonEmpty

Methods

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

SingI (LengthSym0 :: TyFun (NonEmpty a) Nat -> Type)

Defined in Data.Singletons.Prelude.List.NonEmpty

Methods

sing :: Sing LengthSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing FindIndicesSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing FindIndexSym0

SuppressUnusedWarnings ((!!@#@$) :: TyFun [a6989586621679929418] (Nat ~> a6989586621679929418) -> Type)

Defined in Data.Singletons.Prelude.List.Internal

Methods

suppressUnusedWarnings :: ()

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

Defined in Data.Singletons.TypeLits.Internal

Methods

suppressUnusedWarnings :: ()

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

Defined in Data.Singletons.TypeLits.Internal

Methods

suppressUnusedWarnings :: ()

SuppressUnusedWarnings (DivSym1 a3530822107858468865 :: TyFun Nat Nat -> Type)

Defined in Data.Singletons.TypeLits

Methods

suppressUnusedWarnings :: ()

SuppressUnusedWarnings (ModSym1 a3530822107858468865 :: TyFun Nat Nat -> Type)

Defined in Data.Singletons.TypeLits

Methods

suppressUnusedWarnings :: ()

SuppressUnusedWarnings (QuotSym1 a6989586621679478582 :: TyFun Nat Nat -> Type)

Defined in Data.Singletons.TypeLits

Methods

suppressUnusedWarnings :: ()

SuppressUnusedWarnings (RemSym1 a6989586621679478572 :: TyFun Nat Nat -> Type)

Defined in Data.Singletons.TypeLits

Methods

suppressUnusedWarnings :: ()

SuppressUnusedWarnings (QuotRemSym1 a6989586621679478598 :: TyFun Nat (Nat, Nat) -> Type)

Defined in Data.Singletons.TypeLits

Methods

suppressUnusedWarnings :: ()

SuppressUnusedWarnings (DivModSym1 a6989586621679478588 :: TyFun Nat (Nat, Nat) -> Type)

Defined in Data.Singletons.TypeLits

Methods

suppressUnusedWarnings :: ()

SuppressUnusedWarnings (FromIntegerSym0 :: TyFun Nat a6989586621679496884 -> Type)

Defined in Data.Singletons.Prelude.Num

Methods

suppressUnusedWarnings :: ()

SuppressUnusedWarnings (ToEnumSym0 :: TyFun Nat a6989586621679730982 -> Type)

Defined in Data.Singletons.Prelude.Enum

Methods

suppressUnusedWarnings :: ()

SuppressUnusedWarnings (DropSym0 :: TyFun Nat ([a6989586621679929435] ~> [a6989586621679929435]) -> Type)

Defined in Data.Singletons.Prelude.List.Internal

Methods

suppressUnusedWarnings :: ()

SuppressUnusedWarnings (TakeSym0 :: TyFun Nat ([a6989586621679929436] ~> [a6989586621679929436]) -> Type)

Defined in Data.Singletons.Prelude.List.Internal

Methods

suppressUnusedWarnings :: ()

SuppressUnusedWarnings (SplitAtSym0 :: TyFun Nat ([a6989586621679929434] ~> ([a6989586621679929434], [a6989586621679929434])) -> Type)

Defined in Data.Singletons.Prelude.List.Internal

Methods

suppressUnusedWarnings :: ()

SuppressUnusedWarnings (ReplicateSym0 :: TyFun Nat (a6989586621679929420 ~> [a6989586621679929420]) -> Type)

Defined in Data.Singletons.Prelude.List.Internal

Methods

suppressUnusedWarnings :: ()

SuppressUnusedWarnings (ShowsPrecSym0 :: TyFun Nat (a6989586621680248665 ~> (Symbol ~> Symbol)) -> Type)

Defined in Data.Singletons.Prelude.Show

Methods

suppressUnusedWarnings :: ()

SuppressUnusedWarnings (TakeSym0 :: TyFun Nat (NonEmpty a6989586621681089447 ~> [a6989586621681089447]) -> Type)

Defined in Data.Singletons.Prelude.List.NonEmpty

Methods

suppressUnusedWarnings :: ()

SuppressUnusedWarnings (DropSym0 :: TyFun Nat (NonEmpty a6989586621681089446 ~> [a6989586621681089446]) -> Type)

Defined in Data.Singletons.Prelude.List.NonEmpty

Methods

suppressUnusedWarnings :: ()

SuppressUnusedWarnings (SplitAtSym0 :: TyFun Nat (NonEmpty a6989586621681089445 ~> ([a6989586621681089445], [a6989586621681089445])) -> Type)

Defined in Data.Singletons.Prelude.List.NonEmpty

Methods

suppressUnusedWarnings :: ()

SuppressUnusedWarnings (FromEnumSym0 :: TyFun a6989586621679730982 Nat -> Type)

Defined in Data.Singletons.Prelude.Enum

Methods

suppressUnusedWarnings :: ()

SuppressUnusedWarnings (ElemIndicesSym0 :: TyFun a6989586621679929446 ([a6989586621679929446] ~> [Nat]) -> Type)

Defined in Data.Singletons.Prelude.List.Internal

Methods

suppressUnusedWarnings :: ()

SuppressUnusedWarnings (ElemIndexSym0 :: TyFun a6989586621679929447 ([a6989586621679929447] ~> Maybe Nat) -> Type)

Defined in Data.Singletons.Prelude.List.Internal

Methods

suppressUnusedWarnings :: ()

SuppressUnusedWarnings ((!!@#@$) :: TyFun (NonEmpty a6989586621681089425) (Nat ~> a6989586621681089425) -> Type)

Defined in Data.Singletons.Prelude.List.NonEmpty

Methods

suppressUnusedWarnings :: ()

SuppressUnusedWarnings (LengthSym0 :: TyFun (NonEmpty a6989586621681089478) Nat -> Type)

Defined in Data.Singletons.Prelude.List.NonEmpty

Methods

suppressUnusedWarnings :: ()

SuppressUnusedWarnings (FindIndicesSym0 :: TyFun (a6989586621679929444 ~> Bool) ([a6989586621679929444] ~> [Nat]) -> Type)

Defined in Data.Singletons.Prelude.List.Internal

Methods

suppressUnusedWarnings :: ()

SuppressUnusedWarnings (FindIndexSym0 :: TyFun (a6989586621679929445 ~> Bool) ([a6989586621679929445] ~> Maybe Nat) -> Type)

Defined in Data.Singletons.Prelude.List.Internal

Methods

suppressUnusedWarnings :: ()

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (FindIndicesSym1 d)

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (FindIndexSym1 d)

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (ElemIndicesSym1 d)

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (ElemIndexSym1 d)

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

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

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

Defined in Data.Singletons.Prelude.List.NonEmpty

Methods

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

SApplicative m => SingI (ReplicateM_Sym0 :: TyFun Nat (m a ~> m ()) -> Type)

Defined in Data.Singletons.Prelude.Monad

Methods

sing :: Sing ReplicateM_Sym0

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

Defined in Data.Singletons.Prelude.Monad

Methods

sing :: Sing ReplicateMSym0

SuppressUnusedWarnings (FindIndicesSym1 a6989586621679939331 :: TyFun [a6989586621679929444] [Nat] -> Type)

Defined in Data.Singletons.Prelude.List.Internal

Methods

suppressUnusedWarnings :: ()

SuppressUnusedWarnings (ElemIndicesSym1 a6989586621679939357 :: TyFun [a6989586621679929446] [Nat] -> Type)

Defined in Data.Singletons.Prelude.List.Internal

Methods

suppressUnusedWarnings :: ()

SuppressUnusedWarnings (FindIndexSym1 a6989586621679939365 :: TyFun [a6989586621679929445] (Maybe Nat) -> Type)

Defined in Data.Singletons.Prelude.List.Internal

Methods

suppressUnusedWarnings :: ()

SuppressUnusedWarnings (ElemIndexSym1 a6989586621679939373 :: TyFun [a6989586621679929447] (Maybe Nat) -> Type)

Defined in Data.Singletons.Prelude.List.Internal

Methods

suppressUnusedWarnings :: ()

SuppressUnusedWarnings ((!!@#@$$) a6989586621679938708 :: TyFun Nat a6989586621679929418 -> Type)

Defined in Data.Singletons.Prelude.List.Internal

Methods

suppressUnusedWarnings :: ()

SuppressUnusedWarnings ((!!@#@$$) a6989586621681090931 :: TyFun Nat a6989586621681089425 -> Type)

Defined in Data.Singletons.Prelude.List.NonEmpty

Methods

suppressUnusedWarnings :: ()

SuppressUnusedWarnings (ReplicateM_Sym0 :: TyFun Nat (m6989586621681193217 a6989586621681193218 ~> m6989586621681193217 ()) -> Type)

Defined in Data.Singletons.Prelude.Monad

Methods

suppressUnusedWarnings :: ()

SuppressUnusedWarnings (ReplicateMSym0 :: TyFun Nat (m6989586621681193219 a6989586621681193220 ~> m6989586621681193219 [a6989586621681193220]) -> Type)

Defined in Data.Singletons.Prelude.Monad

Methods

suppressUnusedWarnings :: ()

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

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing LengthSym0

SuppressUnusedWarnings (LengthSym0 :: TyFun (t6989586621680438526 a6989586621680438542) Nat -> Type)

Defined in Data.Singletons.Prelude.Foldable

Methods

suppressUnusedWarnings :: ()

type Demote Nat

Defined in Data.Singletons.TypeLits.Internal

type Demote Nat = Natural

data Sing (n :: Nat)

Defined in Data.Singletons.TypeLits.Internal

data Sing (n :: Nat) where

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

type Negate (a :: Nat)

Defined in Data.Singletons.Prelude.Num

type Negate (a :: Nat) = (Error "Cannot negate a natural number" :: Nat)

type Abs (a :: Nat)

Defined in Data.Singletons.Prelude.Num

type Abs (a :: Nat) = a

type Signum (a :: Nat)

Defined in Data.Singletons.Prelude.Num

type Signum (a :: Nat)

type FromInteger a

Defined in Data.Singletons.Prelude.Num

type FromInteger a = a

type Succ (a :: Nat)

Defined in Data.Singletons.Prelude.Enum

type Succ (a :: Nat)

type Pred (a :: Nat)

Defined in Data.Singletons.Prelude.Enum

type Pred (a :: Nat)

type ToEnum a

Defined in Data.Singletons.Prelude.Enum

type ToEnum a

type FromEnum (a :: Nat)

Defined in Data.Singletons.Prelude.Enum

type FromEnum (a :: Nat)

type Show_ (arg :: Nat)

Defined in Data.Singletons.Prelude.Show

type Show_ (arg :: Nat)

type (x :: Nat) == (y :: Nat)

Defined in Data.Singletons.TypeLits.Internal

type (x :: Nat) == (y :: Nat) = DefaultEq x y

type (x :: Nat) /= (y :: Nat)

Defined in Data.Singletons.TypeLits.Internal

type (x :: Nat) /= (y :: Nat) = Not (x == y)

type Compare (a :: Nat) (b :: Nat)

Defined in Data.Singletons.TypeLits.Internal

type Compare (a :: Nat) (b :: Nat) = CmpNat a b

type (arg1 :: Nat) < (arg2 :: Nat)

Defined in Data.Singletons.TypeLits.Internal

type (arg1 :: Nat) < (arg2 :: Nat)

type (arg1 :: Nat) <= (arg2 :: Nat)

Defined in Data.Singletons.TypeLits.Internal

type (arg1 :: Nat) <= (arg2 :: Nat)

type (arg1 :: Nat) > (arg2 :: Nat)

Defined in Data.Singletons.TypeLits.Internal

type (arg1 :: Nat) > (arg2 :: Nat)

type (arg1 :: Nat) >= (arg2 :: Nat)

Defined in Data.Singletons.TypeLits.Internal

type (arg1 :: Nat) >= (arg2 :: Nat)

type Max (arg1 :: Nat) (arg2 :: Nat)

Defined in Data.Singletons.TypeLits.Internal

type Max (arg1 :: Nat) (arg2 :: Nat)

type Min (arg1 :: Nat) (arg2 :: Nat)

Defined in Data.Singletons.TypeLits.Internal

type Min (arg1 :: Nat) (arg2 :: Nat)

type (a :: Nat) + (b :: Nat)

Defined in Data.Singletons.Prelude.Num

type (a :: Nat) + (b :: Nat) = a + b

type (a :: Nat) - (b :: Nat)

Defined in Data.Singletons.Prelude.Num

type (a :: Nat) - (b :: Nat) = a - b

type (a :: Nat) * (b :: Nat)

Defined in Data.Singletons.Prelude.Num

type (a :: Nat) * (b :: Nat) = a * b

type EnumFromTo (a1 :: Nat) (a2 :: Nat)

Defined in Data.Singletons.Prelude.Enum

type EnumFromTo (a1 :: Nat) (a2 :: Nat)

type ShowList (arg1 :: [Nat]) arg2

Defined in Data.Singletons.Prelude.Show

type ShowList (arg1 :: [Nat]) arg2

type Apply KnownNatSym0 (n6989586621679459252 :: Nat)

Defined in Data.Singletons.TypeLits

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

type Apply Log2Sym0 (a3530822107858468865 :: Nat)

Defined in Data.Singletons.TypeLits

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

type EnumFromThenTo (a1 :: Nat) (a2 :: Nat) (a3 :: Nat)

Defined in Data.Singletons.Prelude.Enum

type EnumFromThenTo (a1 :: Nat) (a2 :: Nat) (a3 :: Nat)

type ShowsPrec _ (n :: Nat) x

Defined in Data.Singletons.Prelude.Show

type ShowsPrec _ (n :: Nat) x

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

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)

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)

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)

Defined in Data.Singletons.TypeLits

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

type Apply (QuotSym1 a6989586621679478582 :: TyFun Nat Nat -> Type) (a6989586621679478583 :: Nat)

Defined in Data.Singletons.TypeLits

type Apply (QuotSym1 a6989586621679478582 :: TyFun Nat Nat -> Type) (a6989586621679478583 :: Nat) = Quot a6989586621679478582 a6989586621679478583

type Apply (RemSym1 a6989586621679478572 :: TyFun Nat Nat -> Type) (a6989586621679478573 :: Nat)

Defined in Data.Singletons.TypeLits

type Apply (RemSym1 a6989586621679478572 :: TyFun Nat Nat -> Type) (a6989586621679478573 :: Nat) = Rem a6989586621679478572 a6989586621679478573

type Apply (FromEnumSym0 :: TyFun a Nat -> Type) (arg6989586621679731272 :: a)

Defined in Data.Singletons.Prelude.Enum

type Apply (FromEnumSym0 :: TyFun a Nat -> Type) (arg6989586621679731272 :: a) = FromEnum arg6989586621679731272

type Apply (FromIntegerSym0 :: TyFun Nat k2 -> Type) (arg6989586621679496922 :: Nat)

Defined in Data.Singletons.Prelude.Num

type Apply (FromIntegerSym0 :: TyFun Nat k2 -> Type) (arg6989586621679496922 :: Nat) = (FromInteger arg6989586621679496922 :: k2)

type Apply (ToEnumSym0 :: TyFun Nat k2 -> Type) (arg6989586621679731270 :: Nat)

Defined in Data.Singletons.Prelude.Enum

type Apply (ToEnumSym0 :: TyFun Nat k2 -> Type) (arg6989586621679731270 :: Nat) = (ToEnum arg6989586621679731270 :: k2)

type Apply ((!!@#@$$) a6989586621679938708 :: TyFun Nat a -> Type) (a6989586621679938709 :: Nat)

Defined in Data.Singletons.Prelude.List.Internal

type Apply ((!!@#@$$) a6989586621679938708 :: TyFun Nat a -> Type) (a6989586621679938709 :: Nat) = a6989586621679938708 !! a6989586621679938709

type Apply ((!!@#@$$) a6989586621681090931 :: TyFun Nat a -> Type) (a6989586621681090932 :: Nat)

Defined in Data.Singletons.Prelude.List.NonEmpty

type Apply ((!!@#@$$) a6989586621681090931 :: TyFun Nat a -> Type) (a6989586621681090932 :: Nat) = a6989586621681090931 !! a6989586621681090932

type Apply (LengthSym0 :: TyFun (NonEmpty a) Nat -> Type) (a6989586621681091361 :: NonEmpty a)

Defined in Data.Singletons.Prelude.List.NonEmpty

type Apply (LengthSym0 :: TyFun (NonEmpty a) Nat -> Type) (a6989586621681091361 :: NonEmpty a) = Length a6989586621681091361

type Apply (LengthSym0 :: TyFun (t a) Nat -> Type) (arg6989586621680439191 :: t a)

Defined in Data.Singletons.Prelude.Foldable

type Apply (LengthSym0 :: TyFun (t a) Nat -> Type) (arg6989586621680439191 :: t a) = Length arg6989586621680439191

type Apply (FindIndicesSym1 a6989586621679939331 :: TyFun [a] [Nat] -> Type) (a6989586621679939332 :: [a])

Defined in Data.Singletons.Prelude.List.Internal

type Apply (FindIndicesSym1 a6989586621679939331 :: TyFun [a] [Nat] -> Type) (a6989586621679939332 :: [a]) = FindIndices a6989586621679939331 a6989586621679939332

type Apply (ElemIndicesSym1 a6989586621679939357 :: TyFun [a] [Nat] -> Type) (a6989586621679939358 :: [a])

Defined in Data.Singletons.Prelude.List.Internal

type Apply (ElemIndicesSym1 a6989586621679939357 :: TyFun [a] [Nat] -> Type) (a6989586621679939358 :: [a]) = ElemIndices a6989586621679939357 a6989586621679939358

type Apply (FindIndexSym1 a6989586621679939365 :: TyFun [a] (Maybe Nat) -> Type) (a6989586621679939366 :: [a])

Defined in Data.Singletons.Prelude.List.Internal

type Apply (FindIndexSym1 a6989586621679939365 :: TyFun [a] (Maybe Nat) -> Type) (a6989586621679939366 :: [a]) = FindIndex a6989586621679939365 a6989586621679939366

type Apply (ElemIndexSym1 a6989586621679939373 :: TyFun [a] (Maybe Nat) -> Type) (a6989586621679939374 :: [a])

Defined in Data.Singletons.Prelude.List.Internal

type Apply (ElemIndexSym1 a6989586621679939373 :: TyFun [a] (Maybe Nat) -> Type) (a6989586621679939374 :: [a]) = ElemIndex a6989586621679939373 a6989586621679939374

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

Defined in Data.Singletons.TypeLits.Internal

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

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

Defined in Data.Singletons.TypeLits.Internal

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

type Apply DivSym0 (a3530822107858468865 :: Nat)

Defined in Data.Singletons.TypeLits

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

type Apply ModSym0 (a3530822107858468865 :: Nat)

Defined in Data.Singletons.TypeLits

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

type Apply QuotSym0 (a6989586621679478582 :: Nat)

Defined in Data.Singletons.TypeLits

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

type Apply RemSym0 (a6989586621679478572 :: Nat)

Defined in Data.Singletons.TypeLits

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

type Apply QuotRemSym0 (a6989586621679478598 :: Nat)

Defined in Data.Singletons.TypeLits

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

type Apply DivModSym0 (a6989586621679478588 :: Nat)

Defined in Data.Singletons.TypeLits

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

type Apply (QuotRemSym1 a6989586621679478598 :: TyFun Nat (Nat, Nat) -> Type) (a6989586621679478599 :: Nat)

Defined in Data.Singletons.TypeLits

type Apply (QuotRemSym1 a6989586621679478598 :: TyFun Nat (Nat, Nat) -> Type) (a6989586621679478599 :: Nat) = QuotRem a6989586621679478598 a6989586621679478599

type Apply (DivModSym1 a6989586621679478588 :: TyFun Nat (Nat, Nat) -> Type) (a6989586621679478589 :: Nat)

Defined in Data.Singletons.TypeLits

type Apply (DivModSym1 a6989586621679478588 :: TyFun Nat (Nat, Nat) -> Type) (a6989586621679478589 :: Nat) = DivMod a6989586621679478588 a6989586621679478589

type Apply (DropSym0 :: TyFun Nat ([a6989586621679929435] ~> [a6989586621679929435]) -> Type) (a6989586621679938804 :: Nat)

Defined in Data.Singletons.Prelude.List.Internal

type Apply (DropSym0 :: TyFun Nat ([a6989586621679929435] ~> [a6989586621679929435]) -> Type) (a6989586621679938804 :: Nat) = (DropSym1 a6989586621679938804 a6989586621679929435 :: TyFun [a6989586621679929435] [a6989586621679929435] -> Type)

type Apply (TakeSym0 :: TyFun Nat ([a6989586621679929436] ~> [a6989586621679929436]) -> Type) (a6989586621679938818 :: Nat)

Defined in Data.Singletons.Prelude.List.Internal

type Apply (TakeSym0 :: TyFun Nat ([a6989586621679929436] ~> [a6989586621679929436]) -> Type) (a6989586621679938818 :: Nat) = (TakeSym1 a6989586621679938818 a6989586621679929436 :: TyFun [a6989586621679929436] [a6989586621679929436] -> Type)

type Apply (SplitAtSym0 :: TyFun Nat ([a6989586621679929434] ~> ([a6989586621679929434], [a6989586621679929434])) -> Type) (a6989586621679938832 :: Nat)

Defined in Data.Singletons.Prelude.List.Internal

type Apply (SplitAtSym0 :: TyFun Nat ([a6989586621679929434] ~> ([a6989586621679929434], [a6989586621679929434])) -> Type) (a6989586621679938832 :: Nat) = (SplitAtSym1 a6989586621679938832 a6989586621679929434 :: TyFun [a6989586621679929434] ([a6989586621679929434], [a6989586621679929434]) -> Type)

type Apply (ElemIndicesSym0 :: TyFun a6989586621679929446 ([a6989586621679929446] ~> [Nat]) -> Type) (a6989586621679939357 :: a6989586621679929446)

Defined in Data.Singletons.Prelude.List.Internal

type Apply (ElemIndicesSym0 :: TyFun a6989586621679929446 ([a6989586621679929446] ~> [Nat]) -> Type) (a6989586621679939357 :: a6989586621679929446) = ElemIndicesSym1 a6989586621679939357

type Apply (ElemIndexSym0 :: TyFun a6989586621679929447 ([a6989586621679929447] ~> Maybe Nat) -> Type) (a6989586621679939373 :: a6989586621679929447)

Defined in Data.Singletons.Prelude.List.Internal

type Apply (ElemIndexSym0 :: TyFun a6989586621679929447 ([a6989586621679929447] ~> Maybe Nat) -> Type) (a6989586621679939373 :: a6989586621679929447) = ElemIndexSym1 a6989586621679939373

type Apply (ReplicateSym0 :: TyFun Nat (a6989586621679929420 ~> [a6989586621679929420]) -> Type) (a6989586621679938722 :: Nat)

Defined in Data.Singletons.Prelude.List.Internal

type Apply (ReplicateSym0 :: TyFun Nat (a6989586621679929420 ~> [a6989586621679929420]) -> Type) (a6989586621679938722 :: Nat) = (ReplicateSym1 a6989586621679938722 a6989586621679929420 :: TyFun a6989586621679929420 [a6989586621679929420] -> Type)

type Apply (ShowsPrecSym0 :: TyFun Nat (a6989586621680248665 ~> (Symbol ~> Symbol)) -> Type) (arg6989586621680250615 :: Nat)

Defined in Data.Singletons.Prelude.Show

type Apply (ShowsPrecSym0 :: TyFun Nat (a6989586621680248665 ~> (Symbol ~> Symbol)) -> Type) (arg6989586621680250615 :: Nat) = (ShowsPrecSym1 arg6989586621680250615 a6989586621680248665 :: TyFun a6989586621680248665 (Symbol ~> Symbol) -> Type)

type Apply (TakeSym0 :: TyFun Nat (NonEmpty a6989586621681089447 ~> [a6989586621681089447]) -> Type) (a6989586621681091091 :: Nat)

Defined in Data.Singletons.Prelude.List.NonEmpty

type Apply (TakeSym0 :: TyFun Nat (NonEmpty a6989586621681089447 ~> [a6989586621681089447]) -> Type) (a6989586621681091091 :: Nat) = (TakeSym1 a6989586621681091091 a6989586621681089447 :: TyFun (NonEmpty a6989586621681089447) [a6989586621681089447] -> Type)

type Apply (DropSym0 :: TyFun Nat (NonEmpty a6989586621681089446 ~> [a6989586621681089446]) -> Type) (a6989586621681091099 :: Nat)

Defined in Data.Singletons.Prelude.List.NonEmpty

type Apply (DropSym0 :: TyFun Nat (NonEmpty a6989586621681089446 ~> [a6989586621681089446]) -> Type) (a6989586621681091099 :: Nat) = (DropSym1 a6989586621681091099 a6989586621681089446 :: TyFun (NonEmpty a6989586621681089446) [a6989586621681089446] -> Type)

type Apply (SplitAtSym0 :: TyFun Nat (NonEmpty a6989586621681089445 ~> ([a6989586621681089445], [a6989586621681089445])) -> Type) (a6989586621681091107 :: Nat)

Defined in Data.Singletons.Prelude.List.NonEmpty

type Apply (SplitAtSym0 :: TyFun Nat (NonEmpty a6989586621681089445 ~> ([a6989586621681089445], [a6989586621681089445])) -> Type) (a6989586621681091107 :: Nat) = (SplitAtSym1 a6989586621681091107 a6989586621681089445 :: TyFun (NonEmpty a6989586621681089445) ([a6989586621681089445], [a6989586621681089445]) -> Type)

type Apply (ReplicateM_Sym0 :: TyFun Nat (m6989586621681193217 a6989586621681193218 ~> m6989586621681193217 ()) -> Type) (a6989586621681193593 :: Nat)

Defined in Data.Singletons.Prelude.Monad

type Apply (ReplicateM_Sym0 :: TyFun Nat (m6989586621681193217 a6989586621681193218 ~> m6989586621681193217 ()) -> Type) (a6989586621681193593 :: Nat) = (ReplicateM_Sym1 a6989586621681193593 a6989586621681193218 m6989586621681193217 :: TyFun (m6989586621681193217 a6989586621681193218) (m6989586621681193217 ()) -> Type)

type Apply (ReplicateMSym0 :: TyFun Nat (m6989586621681193219 a6989586621681193220 ~> m6989586621681193219 [a6989586621681193220]) -> Type) (a6989586621681193612 :: Nat)

Defined in Data.Singletons.Prelude.Monad

type Apply (ReplicateMSym0 :: TyFun Nat (m6989586621681193219 a6989586621681193220 ~> m6989586621681193219 [a6989586621681193220]) -> Type) (a6989586621681193612 :: Nat) = (ReplicateMSym1 a6989586621681193612 a6989586621681193220 m6989586621681193219 :: TyFun (m6989586621681193219 a6989586621681193220) (m6989586621681193219 [a6989586621681193220]) -> Type)

type Apply ((!!@#@$) :: TyFun [a6989586621679929418] (Nat ~> a6989586621679929418) -> Type) (a6989586621679938708 :: [a6989586621679929418])

Defined in Data.Singletons.Prelude.List.Internal

type Apply ((!!@#@$) :: TyFun [a6989586621679929418] (Nat ~> a6989586621679929418) -> Type) (a6989586621679938708 :: [a6989586621679929418]) = (!!@#@$$) a6989586621679938708

type Apply ((!!@#@$) :: TyFun (NonEmpty a6989586621681089425) (Nat ~> a6989586621681089425) -> Type) (a6989586621681090931 :: NonEmpty a6989586621681089425)

Defined in Data.Singletons.Prelude.List.NonEmpty

type Apply ((!!@#@$) :: TyFun (NonEmpty a6989586621681089425) (Nat ~> a6989586621681089425) -> Type) (a6989586621681090931 :: NonEmpty a6989586621681089425) = (!!@#@$$) a6989586621681090931

type Apply (FindIndicesSym0 :: TyFun (a6989586621679929444 ~> Bool) ([a6989586621679929444] ~> [Nat]) -> Type) (a6989586621679939331 :: a6989586621679929444 ~> Bool)

Defined in Data.Singletons.Prelude.List.Internal

type Apply (FindIndicesSym0 :: TyFun (a6989586621679929444 ~> Bool) ([a6989586621679929444] ~> [Nat]) -> Type) (a6989586621679939331 :: a6989586621679929444 ~> Bool) = FindIndicesSym1 a6989586621679939331

type Apply (FindIndexSym0 :: TyFun (a6989586621679929445 ~> Bool) ([a6989586621679929445] ~> Maybe Nat) -> Type) (a6989586621679939365 :: a6989586621679929445 ~> Bool)

Defined in Data.Singletons.Prelude.List.Internal

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

data Symbol

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

Instances

Eq Symbol

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.

Defined in Data.Singletons.TypeLits

Methods

(==) :: Symbol -> Symbol -> Bool

(/=) :: Symbol -> Symbol -> Bool

Ord Symbol

Defined in Data.Singletons.TypeLits

Methods

compare :: Symbol -> Symbol -> Ordering

(<) :: Symbol -> Symbol -> Bool

(<=) :: Symbol -> Symbol -> Bool

(>) :: Symbol -> Symbol -> Bool

(>=) :: Symbol -> Symbol -> Bool

max :: Symbol -> Symbol -> Symbol

min :: Symbol -> Symbol -> Symbol

Show Symbol

Defined in Data.Singletons.TypeLits

Methods

showsPrec :: Int -> Symbol -> ShowS

show :: Symbol -> String

showList :: [Symbol] -> ShowS

IsString Symbol

Defined in Data.Singletons.TypeLits

Methods

fromString :: String -> Symbol

Semigroup Symbol

Defined in Data.Singletons.TypeLits

Methods

(<>) :: Symbol -> Symbol -> Symbol

sconcat :: NonEmpty Symbol -> Symbol

stimes :: Integral b => b -> Symbol -> Symbol

Monoid Symbol

Defined in Data.Singletons.TypeLits

Methods

mempty :: Symbol

mappend :: Symbol -> Symbol -> Symbol

mconcat :: [Symbol] -> Symbol

SingKind Symbol

Since: base-4.9.0.0

Defined in GHC.Generics

Associated Types

type DemoteRep Symbol :: Type

Methods

fromSing :: Sing a -> DemoteRep Symbol

SingKind Symbol

Defined in Data.Singletons.TypeLits.Internal

Associated Types

type Demote Symbol = (r :: Type)

Methods

fromSing :: Sing a -> Demote Symbol

toSing :: Demote Symbol -> SomeSing Symbol

SingKind PErrorMessage

Defined in Data.Singletons.TypeError

Associated Types

type Demote PErrorMessage = (r :: Type)

Methods

fromSing :: Sing a -> Demote PErrorMessage

toSing :: Demote PErrorMessage -> SomeSing PErrorMessage

SDecide Symbol

Defined in Data.Singletons.TypeLits.Internal

Methods

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

PEq Symbol

Defined in Data.Singletons.TypeLits.Internal

Associated Types

type x == y :: Bool

type x /= y :: Bool

SEq Symbol

Defined in Data.Singletons.TypeLits.Internal

Methods

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

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

SOrd Symbol

Defined in Data.Singletons.TypeLits.Internal

Methods

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

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

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

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

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

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

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

POrd Symbol

Defined in Data.Singletons.TypeLits.Internal

Associated Types

type Compare arg arg :: Ordering

type arg < arg :: Bool

type arg <= arg :: Bool

type arg > arg :: Bool

type arg >= arg :: Bool

type Max arg arg :: a

type Min arg arg :: a

SSemigroup Symbol

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

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

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

PSemigroup Symbol

Defined in Data.Singletons.Prelude.Semigroup.Internal

Associated Types

type arg <> arg :: a

type Sconcat arg :: a

SShow Symbol

Defined in Data.Singletons.Prelude.Show

Methods

sShowsPrec :: Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply ShowsPrecSym0 t) t) t)

sShow_ :: Sing t -> Sing (Apply Show_Sym0 t)

sShowList :: Sing t -> Sing t -> Sing (Apply (Apply ShowListSym0 t) t)

PShow Symbol

Defined in Data.Singletons.Prelude.Show

Associated Types

type ShowsPrec arg arg arg :: Symbol

type Show_ arg :: Symbol

type ShowList arg arg :: Symbol

SMonoid Symbol

Defined in Data.Singletons.Prelude.Monoid

Methods

sMempty :: Sing MemptySym0

sMappend :: Sing t -> Sing t -> Sing (Apply (Apply MappendSym0 t) t)

sMconcat :: Sing t -> Sing (Apply MconcatSym0 t)

PMonoid Symbol

Defined in Data.Singletons.Prelude.Monoid

Associated Types

type Mempty :: a

type Mappend arg arg :: a

type Mconcat arg :: a

SIsString Symbol

Defined in Data.Singletons.Prelude.IsString

Methods

sFromString :: Sing t -> Sing (Apply FromStringSym0 t)

PIsString Symbol

Defined in Data.Singletons.Prelude.IsString

Associated Types

type FromString arg :: a

KnownSymbol a => SingI (a :: Symbol)

Since: base-4.9.0.0

Defined in GHC.Generics

Methods

sing :: Sing a

KnownSymbol n => SingI (n :: Symbol)

Defined in Data.Singletons.TypeLits.Internal

Methods

sing :: Sing n

SingI t => SingI (Text t :: ErrorMessage' Symbol)

Defined in Data.Singletons.TypeError

Methods

sing :: Sing (Text t)

SingI ty => SingI (ShowType ty :: ErrorMessage' Symbol)

Defined in Data.Singletons.TypeError

Methods

sing :: Sing (ShowType ty)

(SingI e1, SingI e2) => SingI (e1 :<>: e2 :: ErrorMessage' Symbol)

Defined in Data.Singletons.TypeError

Methods

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

(SingI e1, SingI e2) => SingI (e1 :$$: e2 :: ErrorMessage' Symbol)

Defined in Data.Singletons.TypeError

Methods

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

Show (SSymbol s)

Defined in Data.Singletons.ShowSing

Methods

showsPrec :: Int -> SSymbol s -> ShowS

show :: SSymbol s -> String

showList :: [SSymbol s] -> ShowS

SingI ShowParenSym0

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing ShowParenSym0

SingI UnlinesSym0

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing UnlinesSym0

SingI UnwordsSym0

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing UnwordsSym0

SingI ShowCommaSpaceSym0

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing ShowCommaSpaceSym0

SingI ShowSpaceSym0

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing ShowSpaceSym0

SingI ShowCharSym0

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing ShowCharSym0

SingI ShowStringSym0

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing ShowStringSym0

SuppressUnusedWarnings ShowParenSym0

Defined in Data.Singletons.Prelude.Show

Methods

suppressUnusedWarnings :: ()

SuppressUnusedWarnings UnlinesSym0

Defined in Data.Singletons.Prelude.List.Internal

Methods

suppressUnusedWarnings :: ()

SuppressUnusedWarnings UnwordsSym0

Defined in Data.Singletons.Prelude.List.Internal

Methods

suppressUnusedWarnings :: ()

SuppressUnusedWarnings KnownSymbolSym0

Defined in Data.Singletons.TypeLits

Methods

suppressUnusedWarnings :: ()

SuppressUnusedWarnings ShowCommaSpaceSym0

Defined in Data.Singletons.Prelude.Show

Methods

suppressUnusedWarnings :: ()

SuppressUnusedWarnings ShowSpaceSym0

Defined in Data.Singletons.Prelude.Show

Methods

suppressUnusedWarnings :: ()

SuppressUnusedWarnings ShowCharSym0

Defined in Data.Singletons.Prelude.Show

Methods

suppressUnusedWarnings :: ()

SuppressUnusedWarnings ShowStringSym0

Defined in Data.Singletons.Prelude.Show

Methods

suppressUnusedWarnings :: ()

SingI (TypeErrorSym0 :: TyFun PErrorMessage b6989586621681244485 -> Type)

Defined in Data.Singletons.TypeError

Methods

sing :: Sing TypeErrorSym0

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

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing ShowListSym0

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

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing ShowsPrecSym0

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

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing (ShowCharSym1 d)

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

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing (ShowStringSym1 d)

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

Defined in Data.Singletons.Prelude.IsString

Methods

sing :: Sing FromStringSym0

SingI (TextSym0 :: TyFun Symbol (ErrorMessage' Symbol) -> Type)

Defined in Data.Singletons.TypeError

Methods

sing :: Sing TextSym0

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

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing ShowsSym0

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

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing Show_Sym0

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

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing (ShowParenSym1 d)

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

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing ShowListWithSym0

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

Defined in Data.Singletons.TypeError

Methods

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

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

Defined in Data.Singletons.TypeError

Methods

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

SuppressUnusedWarnings (ShowListSym0 :: TyFun [a6989586621680248665] (Symbol ~> Symbol) -> Type)

Defined in Data.Singletons.Prelude.Show

Methods

suppressUnusedWarnings :: ()

SuppressUnusedWarnings (ShowsPrecSym0 :: TyFun Nat (a6989586621680248665 ~> (Symbol ~> Symbol)) -> Type)

Defined in Data.Singletons.Prelude.Show

Methods

suppressUnusedWarnings :: ()

SuppressUnusedWarnings (ShowCharSym1 a6989586621680250549 :: TyFun Symbol Symbol -> Type)

Defined in Data.Singletons.Prelude.Show

Methods

suppressUnusedWarnings :: ()

SuppressUnusedWarnings (ShowStringSym1 a6989586621680250534 :: TyFun Symbol Symbol -> Type)

Defined in Data.Singletons.Prelude.Show

Methods

suppressUnusedWarnings :: ()

SuppressUnusedWarnings (FromStringSym0 :: TyFun Symbol a6989586621681182111 -> Type)

Defined in Data.Singletons.Prelude.IsString

Methods

suppressUnusedWarnings :: ()

SuppressUnusedWarnings (Show_Sym0 :: TyFun a6989586621680248665 Symbol -> Type)

Defined in Data.Singletons.Prelude.Show

Methods

suppressUnusedWarnings :: ()

SuppressUnusedWarnings (ShowsSym0 :: TyFun a6989586621680248650 (Symbol ~> Symbol) -> Type)

Defined in Data.Singletons.Prelude.Show

Methods

suppressUnusedWarnings :: ()

SuppressUnusedWarnings (ShowParenSym1 a6989586621680250555 :: TyFun (Symbol ~> Symbol) (Symbol ~> Symbol) -> Type)

Defined in Data.Singletons.Prelude.Show

Methods

suppressUnusedWarnings :: ()

SuppressUnusedWarnings (ShowListWithSym0 :: TyFun (a6989586621680248649 ~> (Symbol ~> Symbol)) ([a6989586621680248649] ~> (Symbol ~> Symbol)) -> Type)

Defined in Data.Singletons.Prelude.Show

Methods

suppressUnusedWarnings :: ()

SuppressUnusedWarnings (TypeErrorSym0 :: TyFun PErrorMessage b6989586621681244485 -> Type)

Defined in Data.Singletons.TypeError

Methods

suppressUnusedWarnings :: ()

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

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing (ShowListWithSym1 d)

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

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing (ShowListSym1 d)

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

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing (ShowsSym1 d)

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

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing (ShowParenSym2 d1 d2)

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

Defined in Data.Singletons.TypeLits.Internal

Methods

sing :: Sing ErrorSym0

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

Defined in Data.Singletons.TypeLits.Internal

Methods

sing :: Sing ErrorWithoutStackTraceSym0

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

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing (ShowsPrecSym1 d a)

SingI (ShowTypeSym0 :: TyFun t (ErrorMessage' Symbol) -> Type)

Defined in Data.Singletons.TypeError

Methods

sing :: Sing ShowTypeSym0

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

Defined in Data.Singletons.TypeError

Methods

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

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

Defined in Data.Singletons.TypeError

Methods

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

SuppressUnusedWarnings (ShowListWithSym1 a6989586621680250587 :: TyFun [a6989586621680248649] (Symbol ~> Symbol) -> Type)

Defined in Data.Singletons.Prelude.Show

Methods

suppressUnusedWarnings :: ()

SuppressUnusedWarnings (ShowListSym1 arg6989586621680250623 :: TyFun Symbol Symbol -> Type)

Defined in Data.Singletons.Prelude.Show

Methods

suppressUnusedWarnings :: ()

SuppressUnusedWarnings (ShowsSym1 a6989586621680250607 :: TyFun Symbol Symbol -> Type)

Defined in Data.Singletons.Prelude.Show

Methods

suppressUnusedWarnings :: ()

SuppressUnusedWarnings (ShowParenSym2 a6989586621680250556 a6989586621680250555 :: TyFun Symbol Symbol -> Type)

Defined in Data.Singletons.Prelude.Show

Methods

suppressUnusedWarnings :: ()

SuppressUnusedWarnings (ShowsPrecSym1 arg6989586621680250615 a6989586621680248665 :: TyFun a6989586621680248665 (Symbol ~> Symbol) -> Type)

Defined in Data.Singletons.Prelude.Show

Methods

suppressUnusedWarnings :: ()

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

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing (ShowsPrecSym2 d1 d2)

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

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing (ShowListWithSym2 d1 d2)

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

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing FailSym0

SingI (TyCon1 (Text :: Symbol -> ErrorMessage' Symbol))

Defined in Data.Singletons.TypeError

Methods

sing :: Sing (TyCon1 Text)

SingI (TyCon1 (ShowType :: t -> ErrorMessage' Symbol) :: t ~> ErrorMessage' Symbol)

Defined in Data.Singletons.TypeError

Methods

sing :: Sing (TyCon1 ShowType)

SingI x => SingI (TyCon1 ((:<>:) x) :: ErrorMessage' Symbol ~> ErrorMessage' Symbol)

Defined in Data.Singletons.TypeError

Methods

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

SingI x => SingI (TyCon1 ((:$$:) x) :: ErrorMessage' Symbol ~> ErrorMessage' Symbol)

Defined in Data.Singletons.TypeError

Methods

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

SuppressUnusedWarnings (ShowsPrecSym2 arg6989586621680250616 arg6989586621680250615 :: TyFun Symbol Symbol -> Type)

Defined in Data.Singletons.Prelude.Show

Methods

suppressUnusedWarnings :: ()

SuppressUnusedWarnings (ShowListWithSym2 a6989586621680250588 a6989586621680250587 :: TyFun Symbol Symbol -> Type)

Defined in Data.Singletons.Prelude.Show

Methods

suppressUnusedWarnings :: ()

SuppressUnusedWarnings (FailSym0 :: TyFun Symbol (m6989586621679536072 a6989586621679536078) -> Type)

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

suppressUnusedWarnings :: ()

SingI (TyCon2 ((:<>:) :: ErrorMessage' Symbol -> ErrorMessage' Symbol -> ErrorMessage' Symbol))

Defined in Data.Singletons.TypeError

Methods

sing :: Sing (TyCon2 (:<>:))

SingI (TyCon2 ((:$$:) :: ErrorMessage' Symbol -> ErrorMessage' Symbol -> ErrorMessage' Symbol))

Defined in Data.Singletons.TypeError

Methods

sing :: Sing (TyCon2 (:$$:))

data Sing (s :: Symbol)

Defined in GHC.Generics

data Sing (s :: Symbol) where

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

type DemoteRep Symbol

Defined in GHC.Generics

type DemoteRep Symbol = String

type Demote Symbol

Defined in Data.Singletons.TypeLits.Internal

type Demote Symbol = Text

type Demote PErrorMessage

Defined in Data.Singletons.TypeError

type Demote PErrorMessage = ErrorMessage

data Sing (n :: Symbol)

Defined in Data.Singletons.TypeLits.Internal

data Sing (n :: Symbol) where

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

data Sing (a :: PErrorMessage)

Defined in Data.Singletons.TypeError

data Sing (a :: PErrorMessage) where

• SText :: forall (a :: PErrorMessage) (t :: Symbol). Sing t -> Sing (Text t)
• SShowType :: forall (a :: PErrorMessage) t (ty :: t). Sing ty -> Sing (ShowType ty :: ErrorMessage' Symbol)
• (:%<>:) :: forall (a :: PErrorMessage) (e1 :: ErrorMessage' Symbol) (e2 :: ErrorMessage' Symbol). Sing e1 -> Sing e2 -> Sing (e1 :<>: e2)
• (:%$$:) :: forall (a :: PErrorMessage) (e1 :: ErrorMessage' Symbol) (e2 :: ErrorMessage' Symbol). Sing e1 -> Sing e2 -> Sing (e1 :$$: e2)

type Mempty

Defined in Data.Singletons.Prelude.Monoid

type Mempty

type Sconcat (arg :: NonEmpty Symbol)

Defined in Data.Singletons.Prelude.Semigroup.Internal

type Sconcat (arg :: NonEmpty Symbol)

type Show_ (arg :: Symbol)

Defined in Data.Singletons.Prelude.Show

type Show_ (arg :: Symbol)

type Mconcat (arg :: [Symbol])

Defined in Data.Singletons.Prelude.Monoid

type Mconcat (arg :: [Symbol])

type FromString a

Defined in Data.Singletons.Prelude.IsString

type FromString a = a

type (x :: Symbol) == (y :: Symbol)

Defined in Data.Singletons.TypeLits.Internal

type (x :: Symbol) == (y :: Symbol) = DefaultEq x y

type (x :: Symbol) /= (y :: Symbol)

Defined in Data.Singletons.TypeLits.Internal

type (x :: Symbol) /= (y :: Symbol) = Not (x == y)

type Compare (a :: Symbol) (b :: Symbol)

Defined in Data.Singletons.TypeLits.Internal

type Compare (a :: Symbol) (b :: Symbol) = CmpSymbol a b

type (arg1 :: Symbol) < (arg2 :: Symbol)

Defined in Data.Singletons.TypeLits.Internal

type (arg1 :: Symbol) < (arg2 :: Symbol)

type (arg1 :: Symbol) <= (arg2 :: Symbol)

Defined in Data.Singletons.TypeLits.Internal

type (arg1 :: Symbol) <= (arg2 :: Symbol)

type (arg1 :: Symbol) > (arg2 :: Symbol)

Defined in Data.Singletons.TypeLits.Internal

type (arg1 :: Symbol) > (arg2 :: Symbol)

type (arg1 :: Symbol) >= (arg2 :: Symbol)

Defined in Data.Singletons.TypeLits.Internal

type (arg1 :: Symbol) >= (arg2 :: Symbol)

type Max (arg1 :: Symbol) (arg2 :: Symbol)

Defined in Data.Singletons.TypeLits.Internal

type Max (arg1 :: Symbol) (arg2 :: Symbol)

type Min (arg1 :: Symbol) (arg2 :: Symbol)

Defined in Data.Singletons.TypeLits.Internal

type Min (arg1 :: Symbol) (arg2 :: Symbol)

type (a :: Symbol) <> (b :: Symbol)

Defined in Data.Singletons.Prelude.Semigroup.Internal

type (a :: Symbol) <> (b :: Symbol) = AppendSymbol a b

type ShowList (arg1 :: [Symbol]) arg2

Defined in Data.Singletons.Prelude.Show

type ShowList (arg1 :: [Symbol]) arg2

type Mappend (arg1 :: Symbol) (arg2 :: Symbol)

Defined in Data.Singletons.Prelude.Monoid

type Mappend (arg1 :: Symbol) (arg2 :: Symbol)

type Apply KnownSymbolSym0 (n6989586621679459192 :: Symbol)

Defined in Data.Singletons.TypeLits

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

type Apply ShowCommaSpaceSym0 (a6989586621680250542 :: Symbol)

Defined in Data.Singletons.Prelude.Show

type Apply ShowCommaSpaceSym0 (a6989586621680250542 :: Symbol) = ShowCommaSpace a6989586621680250542

type Apply ShowSpaceSym0 (a6989586621680250521 :: Symbol)

Defined in Data.Singletons.Prelude.Show

type Apply ShowSpaceSym0 (a6989586621680250521 :: Symbol) = ShowSpace a6989586621680250521

type ShowsPrec a1 (a2 :: Symbol) a3

Defined in Data.Singletons.Prelude.Show

type ShowsPrec a1 (a2 :: Symbol) a3

type Apply (ShowCharSym1 a6989586621680250549 :: TyFun Symbol Symbol -> Type) (a6989586621680250550 :: Symbol)

Defined in Data.Singletons.Prelude.Show

type Apply (ShowCharSym1 a6989586621680250549 :: TyFun Symbol Symbol -> Type) (a6989586621680250550 :: Symbol) = ShowChar a6989586621680250549 a6989586621680250550

type Apply (ShowStringSym1 a6989586621680250534 :: TyFun Symbol Symbol -> Type) (a6989586621680250535 :: Symbol)

Defined in Data.Singletons.Prelude.Show

type Apply (ShowStringSym1 a6989586621680250534 :: TyFun Symbol Symbol -> Type) (a6989586621680250535 :: Symbol) = ShowString a6989586621680250534 a6989586621680250535

type Apply (Show_Sym0 :: TyFun a Symbol -> Type) (arg6989586621680250621 :: a)

Defined in Data.Singletons.Prelude.Show

type Apply (Show_Sym0 :: TyFun a Symbol -> Type) (arg6989586621680250621 :: a) = Show_ arg6989586621680250621

type Apply (FromStringSym0 :: TyFun Symbol k2 -> Type) (arg6989586621681182147 :: Symbol)

Defined in Data.Singletons.Prelude.IsString

type Apply (FromStringSym0 :: TyFun Symbol k2 -> Type) (arg6989586621681182147 :: Symbol) = (FromString arg6989586621681182147 :: k2)

type Apply (TypeErrorSym0 :: TyFun PErrorMessage k2 -> Type) (a6989586621681244486 :: PErrorMessage)

Defined in Data.Singletons.TypeError

type Apply (TypeErrorSym0 :: TyFun PErrorMessage k2 -> Type) (a6989586621681244486 :: PErrorMessage) = (TypeError a6989586621681244486 :: k2)

type Apply (ShowListSym1 arg6989586621680250623 :: TyFun Symbol Symbol -> Type) (arg6989586621680250624 :: Symbol)

Defined in Data.Singletons.Prelude.Show

type Apply (ShowListSym1 arg6989586621680250623 :: TyFun Symbol Symbol -> Type) (arg6989586621680250624 :: Symbol) = ShowList arg6989586621680250623 arg6989586621680250624

type Apply (ShowsSym1 a6989586621680250607 :: TyFun Symbol Symbol -> Type) (a6989586621680250608 :: Symbol)

Defined in Data.Singletons.Prelude.Show

type Apply (ShowsSym1 a6989586621680250607 :: TyFun Symbol Symbol -> Type) (a6989586621680250608 :: Symbol) = Shows a6989586621680250607 a6989586621680250608

type Apply (ShowParenSym2 a6989586621680250556 a6989586621680250555 :: TyFun Symbol Symbol -> Type) (a6989586621680250557 :: Symbol)

Defined in Data.Singletons.Prelude.Show

type Apply (ShowParenSym2 a6989586621680250556 a6989586621680250555 :: TyFun Symbol Symbol -> Type) (a6989586621680250557 :: Symbol) = ShowParen a6989586621680250556 a6989586621680250555 a6989586621680250557

type Apply (ShowsPrecSym2 arg6989586621680250616 arg6989586621680250615 :: TyFun Symbol Symbol -> Type) (arg6989586621680250617 :: Symbol)

Defined in Data.Singletons.Prelude.Show

type Apply (ShowsPrecSym2 arg6989586621680250616 arg6989586621680250615 :: TyFun Symbol Symbol -> Type) (arg6989586621680250617 :: Symbol) = ShowsPrec arg6989586621680250616 arg6989586621680250615 arg6989586621680250617

type Apply (ShowListWithSym2 a6989586621680250588 a6989586621680250587 :: TyFun Symbol Symbol -> Type) (a6989586621680250589 :: Symbol)

Defined in Data.Singletons.Prelude.Show

type Apply (ShowListWithSym2 a6989586621680250588 a6989586621680250587 :: TyFun Symbol Symbol -> Type) (a6989586621680250589 :: Symbol) = ShowListWith a6989586621680250588 a6989586621680250587 a6989586621680250589

type Apply UnlinesSym0 (a6989586621679939137 :: [Symbol])

Defined in Data.Singletons.Prelude.List.Internal

type Apply UnlinesSym0 (a6989586621679939137 :: [Symbol]) = Unlines a6989586621679939137

type Apply UnwordsSym0 (a6989586621679939126 :: [Symbol])

Defined in Data.Singletons.Prelude.List.Internal

type Apply UnwordsSym0 (a6989586621679939126 :: [Symbol]) = Unwords a6989586621679939126

type Apply (FailSym0 :: TyFun Symbol (m6989586621679536072 a6989586621679536078) -> Type) (arg6989586621679536554 :: Symbol)

Defined in Data.Singletons.Prelude.Monad.Internal

type Apply (FailSym0 :: TyFun Symbol (m6989586621679536072 a6989586621679536078) -> Type) (arg6989586621679536554 :: Symbol) = (Fail arg6989586621679536554 :: m6989586621679536072 a6989586621679536078)

type Apply ShowCharSym0 (a6989586621680250549 :: Symbol)

Defined in Data.Singletons.Prelude.Show

type Apply ShowCharSym0 (a6989586621680250549 :: Symbol) = ShowCharSym1 a6989586621680250549

type Apply ShowStringSym0 (a6989586621680250534 :: Symbol)

Defined in Data.Singletons.Prelude.Show

type Apply ShowStringSym0 (a6989586621680250534 :: Symbol) = ShowStringSym1 a6989586621680250534

type Apply ShowParenSym0 (a6989586621680250555 :: Bool)

Defined in Data.Singletons.Prelude.Show

type Apply ShowParenSym0 (a6989586621680250555 :: Bool) = ShowParenSym1 a6989586621680250555

type Apply (ShowsSym0 :: TyFun a6989586621680248650 (Symbol ~> Symbol) -> Type) (a6989586621680250607 :: a6989586621680248650)

Defined in Data.Singletons.Prelude.Show

type Apply (ShowsSym0 :: TyFun a6989586621680248650 (Symbol ~> Symbol) -> Type) (a6989586621680250607 :: a6989586621680248650) = ShowsSym1 a6989586621680250607

type Apply (ShowsPrecSym0 :: TyFun Nat (a6989586621680248665 ~> (Symbol ~> Symbol)) -> Type) (arg6989586621680250615 :: Nat)

Defined in Data.Singletons.Prelude.Show

type Apply (ShowsPrecSym0 :: TyFun Nat (a6989586621680248665 ~> (Symbol ~> Symbol)) -> Type) (arg6989586621680250615 :: Nat) = (ShowsPrecSym1 arg6989586621680250615 a6989586621680248665 :: TyFun a6989586621680248665 (Symbol ~> Symbol) -> Type)

type Apply (ShowsPrecSym1 arg6989586621680250615 a6989586621680248665 :: TyFun a6989586621680248665 (Symbol ~> Symbol) -> Type) (arg6989586621680250616 :: a6989586621680248665)

Defined in Data.Singletons.Prelude.Show

type Apply (ShowsPrecSym1 arg6989586621680250615 a6989586621680248665 :: TyFun a6989586621680248665 (Symbol ~> Symbol) -> Type) (arg6989586621680250616 :: a6989586621680248665) = ShowsPrecSym2 arg6989586621680250615 arg6989586621680250616

type Apply (ShowListSym0 :: TyFun [a6989586621680248665] (Symbol ~> Symbol) -> Type) (arg6989586621680250623 :: [a6989586621680248665])

Defined in Data.Singletons.Prelude.Show

type Apply (ShowListSym0 :: TyFun [a6989586621680248665] (Symbol ~> Symbol) -> Type) (arg6989586621680250623 :: [a6989586621680248665]) = ShowListSym1 arg6989586621680250623

type Apply (ShowListWithSym1 a6989586621680250587 :: TyFun [a6989586621680248649] (Symbol ~> Symbol) -> Type) (a6989586621680250588 :: [a6989586621680248649])

Defined in Data.Singletons.Prelude.Show

type Apply (ShowListWithSym1 a6989586621680250587 :: TyFun [a6989586621680248649] (Symbol ~> Symbol) -> Type) (a6989586621680250588 :: [a6989586621680248649]) = ShowListWithSym2 a6989586621680250587 a6989586621680250588

type Apply (ShowListWithSym0 :: TyFun (a6989586621680248649 ~> (Symbol ~> Symbol)) ([a6989586621680248649] ~> (Symbol ~> Symbol)) -> Type) (a6989586621680250587 :: a6989586621680248649 ~> (Symbol ~> Symbol))

Defined in Data.Singletons.Prelude.Show

type Apply (ShowListWithSym0 :: TyFun (a6989586621680248649 ~> (Symbol ~> Symbol)) ([a6989586621680248649] ~> (Symbol ~> Symbol)) -> Type) (a6989586621680250587 :: a6989586621680248649 ~> (Symbol ~> Symbol)) = ShowListWithSym1 a6989586621680250587

type Apply (ShowParenSym1 a6989586621680250555 :: TyFun (Symbol ~> Symbol) (Symbol ~> Symbol) -> Type) (a6989586621680250556 :: Symbol ~> Symbol)

Defined in Data.Singletons.Prelude.Show

type Apply (ShowParenSym1 a6989586621680250555 :: TyFun (Symbol ~> Symbol) (Symbol ~> Symbol) -> Type) (a6989586621680250556 :: Symbol ~> Symbol) = ShowParenSym2 a6989586621680250555 a6989586621680250556

data family Sing :: k -> Type

The singleton kind-indexed data family.

Instances

SDecide k => TestCoercion (Sing :: k -> Type)

Defined in Data.Singletons.Decide

Methods

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

SDecide k => TestEquality (Sing :: k -> Type)

Defined in Data.Singletons.Decide

Methods

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

Show (SSymbol s)

Defined in Data.Singletons.ShowSing

Methods

showsPrec :: Int -> SSymbol s -> ShowS

show :: SSymbol s -> String

showList :: [SSymbol s] -> ShowS

Show (SNat n)

Defined in Data.Singletons.ShowSing

Methods

showsPrec :: Int -> SNat n -> ShowS

show :: SNat n -> String

showList :: [SNat n] -> ShowS

Eq (Sing a)

Defined in Data.Singletons.TypeRepTYPE

Methods

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

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

Ord (Sing a)

Defined in Data.Singletons.TypeRepTYPE

Methods

compare :: Sing a -> Sing a -> Ordering

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

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

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

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

max :: Sing a -> Sing a -> Sing a

min :: Sing a -> Sing a -> Sing a

Show (Sing z)

Defined in Data.Singletons.ShowSing

Methods

showsPrec :: Int -> Sing z -> ShowS

show :: Sing z -> String

showList :: [Sing z] -> ShowS

(ShowSing a, ShowSing [a]) => Show (Sing z)

Defined in Data.Singletons.ShowSing

Methods

showsPrec :: Int -> Sing z -> ShowS

show :: Sing z -> String

showList :: [Sing z] -> ShowS

ShowSing a => Show (Sing z)

Defined in Data.Singletons.ShowSing

Methods

showsPrec :: Int -> Sing z -> ShowS

show :: Sing z -> String

showList :: [Sing z] -> ShowS

Show (Sing z)

Defined in Data.Singletons.ShowSing

Methods

showsPrec :: Int -> Sing z -> ShowS

show :: Sing z -> String

showList :: [Sing z] -> ShowS

(ShowSing a, ShowSing b) => Show (Sing z)

Defined in Data.Singletons.ShowSing

Methods

showsPrec :: Int -> Sing z -> ShowS

show :: Sing z -> String

showList :: [Sing z] -> ShowS

Show (Sing a)

Defined in Data.Singletons.TypeRepTYPE

Methods

showsPrec :: Int -> Sing a -> ShowS

show :: Sing a -> String

showList :: [Sing a] -> ShowS

Show (Sing z)

Defined in Data.Singletons.ShowSing

Methods

showsPrec :: Int -> Sing z -> ShowS

show :: Sing z -> String

showList :: [Sing z] -> ShowS

(ShowSing a, ShowSing b) => Show (Sing z)

Defined in Data.Singletons.ShowSing

Methods

showsPrec :: Int -> Sing z -> ShowS

show :: Sing z -> String

showList :: [Sing z] -> ShowS

(ShowSing a, ShowSing b, ShowSing c) => Show (Sing z)

Defined in Data.Singletons.ShowSing

Methods

showsPrec :: Int -> Sing z -> ShowS

show :: Sing z -> String

showList :: [Sing z] -> ShowS

(ShowSing a, ShowSing b, ShowSing c, ShowSing d) => Show (Sing z)

Defined in Data.Singletons.ShowSing

Methods

showsPrec :: Int -> Sing z -> ShowS

show :: Sing z -> String

showList :: [Sing z] -> ShowS

(ShowSing a, ShowSing b, ShowSing c, ShowSing d, ShowSing e) => Show (Sing z)

Defined in Data.Singletons.ShowSing

Methods

showsPrec :: Int -> Sing z -> ShowS

show :: Sing z -> String

showList :: [Sing z] -> ShowS

(ShowSing a, ShowSing b, ShowSing c, ShowSing d, ShowSing e, ShowSing f) => Show (Sing z)

Defined in Data.Singletons.ShowSing

Methods

showsPrec :: Int -> Sing z -> ShowS

show :: Sing z -> String

showList :: [Sing z] -> ShowS

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

Defined in Data.Singletons.ShowSing

Methods

showsPrec :: Int -> Sing z -> ShowS

show :: Sing z -> String

showList :: [Sing z] -> ShowS

Show (Sing z)

Defined in Data.Singletons.ShowSing

Methods

showsPrec :: Int -> Sing z -> ShowS

show :: Sing z -> String

showList :: [Sing z] -> ShowS

ShowSing a => Show (Sing z)

Defined in Data.Singletons.Prelude.Semigroup

Methods

showsPrec :: Int -> Sing z -> ShowS

show :: Sing z -> String

showList :: [Sing z] -> ShowS

ShowSing a => Show (Sing z)

Defined in Data.Singletons.Prelude.Semigroup

Methods

showsPrec :: Int -> Sing z -> ShowS

show :: Sing z -> String

showList :: [Sing z] -> ShowS

(ShowSing a, ShowSing b) => Show (Sing z)

Defined in Data.Singletons.Prelude.Semigroup

Methods

showsPrec :: Int -> Sing z -> ShowS

show :: Sing z -> String

showList :: [Sing z] -> ShowS

ShowSing a => Show (Sing z)

Defined in Data.Singletons.Prelude.Semigroup

Methods

showsPrec :: Int -> Sing z -> ShowS

show :: Sing z -> String

showList :: [Sing z] -> ShowS

ShowSing a => Show (Sing z)

Defined in Data.Singletons.Prelude.Semigroup

Methods

showsPrec :: Int -> Sing z -> ShowS

show :: Sing z -> String

showList :: [Sing z] -> ShowS

ShowSing m => Show (Sing z)

Defined in Data.Singletons.Prelude.Semigroup

Methods

showsPrec :: Int -> Sing z -> ShowS

show :: Sing z -> String

showList :: [Sing z] -> ShowS

ShowSing (Maybe a) => Show (Sing z)

Defined in Data.Singletons.Prelude.Semigroup

Methods

showsPrec :: Int -> Sing z -> ShowS

show :: Sing z -> String

showList :: [Sing z] -> ShowS

ShowSing a => Show (Sing z)

Defined in Data.Singletons.ShowSing

Methods

showsPrec :: Int -> Sing z -> ShowS

show :: Sing z -> String

showList :: [Sing z] -> ShowS

ShowSing (Maybe a) => Show (Sing z)

Defined in Data.Singletons.Prelude.Monoid

Methods

showsPrec :: Int -> Sing z -> ShowS

show :: Sing z -> String

showList :: [Sing z] -> ShowS

ShowSing (Maybe a) => Show (Sing z)

Defined in Data.Singletons.Prelude.Monoid

Methods

showsPrec :: Int -> Sing z -> ShowS

show :: Sing z -> String

showList :: [Sing z] -> ShowS

ShowSing a => Show (Sing z)

Defined in Data.Singletons.Prelude.Semigroup

Methods

showsPrec :: Int -> Sing z -> ShowS

show :: Sing z -> String

showList :: [Sing z] -> ShowS

ShowSing Bool => Show (Sing z)

Defined in Data.Singletons.Prelude.Semigroup

Methods

showsPrec :: Int -> Sing z -> ShowS

show :: Sing z -> String

showList :: [Sing z] -> ShowS

ShowSing Bool => Show (Sing z)

Defined in Data.Singletons.Prelude.Semigroup

Methods

showsPrec :: Int -> Sing z -> ShowS

show :: Sing z -> String

showList :: [Sing z] -> ShowS

ShowSing a => Show (Sing z)

Defined in Data.Singletons.Prelude.Semigroup

Methods

showsPrec :: Int -> Sing z -> ShowS

show :: Sing z -> String

showList :: [Sing z] -> ShowS

ShowSing a => Show (Sing z)

Defined in Data.Singletons.Prelude.Semigroup

Methods

showsPrec :: Int -> Sing z -> ShowS

show :: Sing z -> String

showList :: [Sing z] -> ShowS

(ShowSing a, ShowSing [a]) => Show (Sing z)

Defined in Data.Singletons.ShowSing

Methods

showsPrec :: Int -> Sing z -> ShowS

show :: Sing z -> String

showList :: [Sing z] -> ShowS

data Sing (a :: Bool)

Defined in Data.Singletons.Prelude.Instances

data Sing (a :: Bool) where

• SFalse :: forall (a :: Bool). Sing False
• STrue :: forall (a :: Bool). Sing True

data Sing (a :: Ordering)

Defined in Data.Singletons.Prelude.Instances

data Sing (a :: Ordering) where

• SLT :: forall (a :: Ordering). Sing LT
• SEQ :: forall (a :: Ordering). Sing EQ
• SGT :: forall (a :: Ordering). Sing GT

data Sing (n :: Nat)

Defined in Data.Singletons.TypeLits.Internal

data Sing (n :: Nat) where

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

data Sing (n :: Symbol)

Defined in Data.Singletons.TypeLits.Internal

data Sing (n :: Symbol) where

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

data Sing (a :: ())

Defined in Data.Singletons.Prelude.Instances

data Sing (a :: ()) where

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

data Sing (a :: Void)

Defined in Data.Singletons.Prelude.Instances

data Sing (a :: Void)

data Sing (a :: All)

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (a :: All) where

• SAll :: forall (a :: All) (n :: Bool). {..} -> Sing (All n)

data Sing (a :: Any)

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (a :: Any) where

• SAny :: forall (a :: Any) (n :: Bool). {..} -> Sing (Any n)

data Sing (a :: PErrorMessage)

Defined in Data.Singletons.TypeError

data Sing (a :: PErrorMessage) where

• SText :: forall (a :: PErrorMessage) (t :: Symbol). Sing t -> Sing (Text t)
• SShowType :: forall (a :: PErrorMessage) t (ty :: t). Sing ty -> Sing (ShowType ty :: ErrorMessage' Symbol)
• (:%<>:) :: forall (a :: PErrorMessage) (e1 :: ErrorMessage' Symbol) (e2 :: ErrorMessage' Symbol). Sing e1 -> Sing e2 -> Sing (e1 :<>: e2)
• (:%$$:) :: forall (a :: PErrorMessage) (e1 :: ErrorMessage' Symbol) (e2 :: ErrorMessage' Symbol). Sing e1 -> Sing e2 -> Sing (e1 :$$: e2)

data Sing (b :: [a])

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)

Defined in Data.Singletons.Prelude.Instances

data Sing (b :: Maybe a) where

• SNothing :: forall a (b :: Maybe a). Sing (Nothing :: Maybe a)
• SJust :: forall a (b :: Maybe a) (n :: a). Sing n -> Sing (Just n)

data Sing (a :: TYPE rep)

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.

Defined in Data.Singletons.TypeRepTYPE

data Sing (a :: TYPE rep) = STypeRep (TypeRep a)

data Sing (b :: Min a)

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: Min a) where

• SMin :: forall a (b :: Min a) (n :: a). {..} -> Sing (Min n)

data Sing (b :: Max a)

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: Max a) where

• SMax :: forall a (b :: Max a) (n :: a). {..} -> Sing (Max n)

data Sing (b :: First a)

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: First a) where

• SFirst :: forall a (b :: First a) (n :: a). {..} -> Sing (First n)

data Sing (b :: Last a)

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: Last a) where

• SLast :: forall a (b :: Last a) (n :: a). {..} -> Sing (Last n)

data Sing (a :: WrappedMonoid m)

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (a :: WrappedMonoid m) where

• SWrapMonoid :: forall m (a :: WrappedMonoid m) (n :: m). {..} -> Sing (WrapMonoid n)

data Sing (b :: Option a)

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: Option a) where

• SOption :: forall a (b :: Option a) (n :: Maybe a). {..} -> Sing (Option n)

data Sing (b :: Identity a)

Defined in Data.Singletons.Prelude.Instances

data Sing (b :: Identity a) where

• SIdentity :: forall a (b :: Identity a) (n :: a). {..} -> Sing (Identity n)

data Sing (b :: First a)

Defined in Data.Singletons.Prelude.Monoid

data Sing (b :: First a) where

• SFirst :: forall a (b :: First a) (n :: Maybe a). {..} -> Sing (First n)

data Sing (b :: Last a)

Defined in Data.Singletons.Prelude.Monoid

data Sing (b :: Last a) where

• SLast :: forall a (b :: Last a) (n :: Maybe a). {..} -> Sing (Last n)

data Sing (b :: Dual a)

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: Dual a) where

• SDual :: forall a (b :: Dual a) (n :: a). {..} -> Sing (Dual n)

data Sing (b :: Sum a)

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: Sum a) where

• SSum :: forall a (b :: Sum a) (n :: a). {..} -> Sing (Sum n)

data Sing (b :: Product a)

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: Product a) where

• SProduct :: forall a (b :: Product a) (n :: a). {..} -> Sing (Product n)

data Sing (b :: Down a)

Defined in Data.Singletons.Prelude.Ord

data Sing (b :: Down a) where

• SDown :: forall a (b :: Down a) (n :: a). Sing n -> Sing (Down n)

data Sing (b :: NonEmpty a)

Defined in Data.Singletons.Prelude.Instances

data Sing (b :: NonEmpty a) where

• (:%|) :: forall a (b :: NonEmpty a) (n :: a) (n :: [a]). Sing n -> Sing n -> Sing (n :| n)

data Sing (c :: Either a b)

Defined in Data.Singletons.Prelude.Instances

data Sing (c :: Either a b) where

• SLeft :: forall a b (c :: Either a b) (n :: a). Sing n -> Sing (Left n :: Either a b)
• SRight :: forall a b (c :: Either a b) (n :: b). Sing n -> Sing (Right n :: Either a b)

data Sing (c :: (a, b))

Defined in Data.Singletons.Prelude.Instances

data Sing (c :: (a, b)) where

• STuple2 :: forall a b (c :: (a, b)) (n :: a) (n :: b). Sing n -> Sing n -> Sing ((,) n n)

data Sing (c :: Arg a b)

Defined in Data.Singletons.Prelude.Semigroup

data Sing (c :: Arg a b) where

• SArg :: forall a b (c :: Arg a b) (n :: a) (n :: b). Sing n -> Sing n -> Sing (Arg n n)

data Sing (f :: k1 ~> k2)

Defined in Data.Singletons.Internal

data Sing (f :: k1 ~> k2) = SLambda {

• applySing :: forall (t :: k1). Sing t -> Sing (f @@ t)

}

data Sing (d :: (a, b, c))

Defined in Data.Singletons.Prelude.Instances

data Sing (d :: (a, b, c)) where

• STuple3 :: forall a b c (d :: (a, b, c)) (n :: a) (n :: b) (n :: c). Sing n -> Sing n -> Sing n -> Sing ((,,) n n n)

data Sing (c :: Const a b)

Defined in Data.Singletons.Prelude.Const

data Sing (c :: Const a b) where

• SConst :: forall k a (b :: k) (c :: Const a b) (a :: a). {..} -> Sing (Const a :: Const a b)

data Sing (e :: (a, b, c, d))

Defined in Data.Singletons.Prelude.Instances

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

• STuple4 :: forall a b c d (e :: (a, b, c, d)) (n :: a) (n :: b) (n :: c) (n :: d). Sing n -> Sing n -> Sing n -> Sing n -> Sing ((,,,) n n n n)

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

Defined in Data.Singletons.Prelude.Instances

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

• STuple5 :: forall a b c d e (f :: (a, b, c, d, e)) (n :: a) (n :: b) (n :: c) (n :: d) (n :: e). Sing n -> Sing n -> Sing n -> Sing n -> Sing n -> Sing ((,,,,) n n n n n)

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

Defined in Data.Singletons.Prelude.Instances

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

• STuple6 :: forall a b c d e f (g :: (a, b, c, d, e, f)) (n :: a) (n :: b) (n :: c) (n :: d) (n :: e) (n :: f). Sing n -> Sing n -> Sing n -> Sing n -> Sing n -> Sing n -> Sing ((,,,,,) n n n n n n)

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

Defined in Data.Singletons.Prelude.Instances

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

• STuple7 :: forall a b c d e f g (h :: (a, b, c, d, e, f, g)) (n :: a) (n :: b) (n :: c) (n :: d) (n :: e) (n :: f) (n :: g). Sing n -> Sing n -> Sing n -> Sing n -> Sing n -> Sing n -> Sing n -> Sing ((,,,,,,) n n n n n n n)

type SNat (x :: Nat) = Sing x

Kind-restricted synonym for Sing for Nats

type SSymbol (x :: Symbol) = Sing x

Kind-restricted synonym for Sing for Symbols

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

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

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

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

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

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

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

The singleton for error

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

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

sErrorWithoutStackTrace :: Sing (str :: Symbol) -> a

The singleton for errorWithoutStackTrace.

type family Undefined :: k where ...

The promotion of undefined.

sUndefined :: HasCallStack => a

The singleton for undefined.

class KnownNat (n :: Nat)

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

Since: base-4.10.0.0

class KnownSymbol (n :: Symbol)

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

Since: base-4.7.0.0

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

Exponentiation of type-level naturals.

Since: base-4.7.0.0

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

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

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

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

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

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)

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

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

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

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

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

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)

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

Equations

Quot a_6989586621679478578 a_6989586621679478580 = Apply (Apply DivSym0 a_6989586621679478578) a_6989586621679478580

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

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

Equations

Rem a_6989586621679478568 a_6989586621679478570 = Apply (Apply ModSym0 a_6989586621679478568) a_6989586621679478570

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

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

Equations

QuotRem a_6989586621679478594 a_6989586621679478596 = Apply (Apply DivModSym0 a_6989586621679478594) a_6989586621679478596

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

Defunctionalization symbols

data ErrorSym0 :: forall k06989586621679458997 k6989586621679458996. (~>) k06989586621679458997 k6989586621679458996

Instances

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

Defined in Data.Singletons.TypeLits.Internal

Methods

sing :: Sing ErrorSym0

SuppressUnusedWarnings (ErrorSym0 :: TyFun k06989586621679458997 k6989586621679458996 -> Type)

Defined in Data.Singletons.TypeLits.Internal

Methods

suppressUnusedWarnings :: ()

type Apply (ErrorSym0 :: TyFun k0 k2 -> Type) (str6989586621679458998 :: k0)

Defined in Data.Singletons.TypeLits.Internal

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

type ErrorSym1 (str6989586621679458998 :: k06989586621679458997) = Error str6989586621679458998

data ErrorWithoutStackTraceSym0 :: forall k06989586621679460047 k6989586621679460046. (~>) k06989586621679460047 k6989586621679460046

Instances

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

Defined in Data.Singletons.TypeLits.Internal

Methods

sing :: Sing ErrorWithoutStackTraceSym0

SuppressUnusedWarnings (ErrorWithoutStackTraceSym0 :: TyFun k06989586621679460047 k6989586621679460046 -> Type)

Defined in Data.Singletons.TypeLits.Internal

Methods

suppressUnusedWarnings :: ()

type Apply (ErrorWithoutStackTraceSym0 :: TyFun k0 k2 -> Type) (str6989586621679460048 :: k0)

Defined in Data.Singletons.TypeLits.Internal

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

type ErrorWithoutStackTraceSym1 (str6989586621679460048 :: k06989586621679460047) = ErrorWithoutStackTrace str6989586621679460048

type UndefinedSym0 = Undefined

data KnownNatSym0 :: (~>) Nat Constraint

Instances

SuppressUnusedWarnings KnownNatSym0

Defined in Data.Singletons.TypeLits

Methods

suppressUnusedWarnings :: ()

type Apply KnownNatSym0 (n6989586621679459252 :: Nat)

Defined in Data.Singletons.TypeLits

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

type KnownNatSym1 (n6989586621679459252 :: Nat) = KnownNat n6989586621679459252

data KnownSymbolSym0 :: (~>) Symbol Constraint

Instances

SuppressUnusedWarnings KnownSymbolSym0

Defined in Data.Singletons.TypeLits

Methods

suppressUnusedWarnings :: ()

type Apply KnownSymbolSym0 (n6989586621679459192 :: Symbol)

Defined in Data.Singletons.TypeLits

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

type KnownSymbolSym1 (n6989586621679459192 :: Symbol) = KnownSymbol n6989586621679459192

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

Instances

SingI (^@#@$)

Defined in Data.Singletons.TypeLits.Internal

Methods

sing :: Sing (^@#@$)

SuppressUnusedWarnings (^@#@$)

Defined in Data.Singletons.TypeLits.Internal

Methods

suppressUnusedWarnings :: ()

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

Defined in Data.Singletons.TypeLits.Internal

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

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

Instances

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

Defined in Data.Singletons.TypeLits.Internal

Methods

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

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

Defined in Data.Singletons.TypeLits.Internal

Methods

suppressUnusedWarnings :: ()

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

Defined in Data.Singletons.TypeLits.Internal

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

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

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

Instances

SingI (<=?@#@$)

Defined in Data.Singletons.TypeLits.Internal

Methods

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

SuppressUnusedWarnings (<=?@#@$)

Defined in Data.Singletons.TypeLits.Internal

Methods

suppressUnusedWarnings :: ()

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

Defined in Data.Singletons.TypeLits.Internal

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

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

Instances

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

Defined in Data.Singletons.TypeLits.Internal

Methods

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

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

Defined in Data.Singletons.TypeLits.Internal

Methods

suppressUnusedWarnings :: ()

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

Defined in Data.Singletons.TypeLits.Internal

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

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

data Log2Sym0 :: (~>) Nat Nat

Instances

SingI Log2Sym0

Defined in Data.Singletons.TypeLits

Methods

sing :: Sing Log2Sym0

SuppressUnusedWarnings Log2Sym0

Defined in Data.Singletons.TypeLits

Methods

suppressUnusedWarnings :: ()

type Apply Log2Sym0 (a3530822107858468865 :: Nat)

Defined in Data.Singletons.TypeLits

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

type Log2Sym1 (a3530822107858468865 :: Nat) = Log2 a3530822107858468865

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

Instances

SingI DivSym0

Defined in Data.Singletons.TypeLits

Methods

sing :: Sing DivSym0

SuppressUnusedWarnings DivSym0

Defined in Data.Singletons.TypeLits

Methods

suppressUnusedWarnings :: ()

type Apply DivSym0 (a3530822107858468865 :: Nat)

Defined in Data.Singletons.TypeLits

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

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

Instances

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

Defined in Data.Singletons.TypeLits

Methods

sing :: Sing (DivSym1 x)

SuppressUnusedWarnings (DivSym1 a3530822107858468865 :: TyFun Nat Nat -> Type)

Defined in Data.Singletons.TypeLits

Methods

suppressUnusedWarnings :: ()

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

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

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

Instances

SingI ModSym0

Defined in Data.Singletons.TypeLits

Methods

sing :: Sing ModSym0

SuppressUnusedWarnings ModSym0

Defined in Data.Singletons.TypeLits

Methods

suppressUnusedWarnings :: ()

type Apply ModSym0 (a3530822107858468865 :: Nat)

Defined in Data.Singletons.TypeLits

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

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

Instances

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

Defined in Data.Singletons.TypeLits

Methods

sing :: Sing (ModSym1 x)

SuppressUnusedWarnings (ModSym1 a3530822107858468865 :: TyFun Nat Nat -> Type)

Defined in Data.Singletons.TypeLits

Methods

suppressUnusedWarnings :: ()

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

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

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

Instances

SuppressUnusedWarnings DivModSym0

Defined in Data.Singletons.TypeLits

Methods

suppressUnusedWarnings :: ()

type Apply DivModSym0 (a6989586621679478588 :: Nat)

Defined in Data.Singletons.TypeLits

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

data DivModSym1 (a6989586621679478588 :: Nat) :: (~>) Nat (Nat, Nat)

Instances

SuppressUnusedWarnings (DivModSym1 a6989586621679478588 :: TyFun Nat (Nat, Nat) -> Type)

Defined in Data.Singletons.TypeLits

Methods

suppressUnusedWarnings :: ()

type Apply (DivModSym1 a6989586621679478588 :: TyFun Nat (Nat, Nat) -> Type) (a6989586621679478589 :: Nat)

Defined in Data.Singletons.TypeLits

type Apply (DivModSym1 a6989586621679478588 :: TyFun Nat (Nat, Nat) -> Type) (a6989586621679478589 :: Nat) = DivMod a6989586621679478588 a6989586621679478589

type DivModSym2 (a6989586621679478588 :: Nat) (a6989586621679478589 :: Nat) = DivMod a6989586621679478588 a6989586621679478589

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

Instances

SuppressUnusedWarnings QuotSym0

Defined in Data.Singletons.TypeLits

Methods

suppressUnusedWarnings :: ()

type Apply QuotSym0 (a6989586621679478582 :: Nat)

Defined in Data.Singletons.TypeLits

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

data QuotSym1 (a6989586621679478582 :: Nat) :: (~>) Nat Nat infixl 7

Instances

SuppressUnusedWarnings (QuotSym1 a6989586621679478582 :: TyFun Nat Nat -> Type)

Defined in Data.Singletons.TypeLits

Methods

suppressUnusedWarnings :: ()

type Apply (QuotSym1 a6989586621679478582 :: TyFun Nat Nat -> Type) (a6989586621679478583 :: Nat)

Defined in Data.Singletons.TypeLits

type Apply (QuotSym1 a6989586621679478582 :: TyFun Nat Nat -> Type) (a6989586621679478583 :: Nat) = Quot a6989586621679478582 a6989586621679478583

type QuotSym2 (a6989586621679478582 :: Nat) (a6989586621679478583 :: Nat) = Quot a6989586621679478582 a6989586621679478583

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

Instances

SuppressUnusedWarnings RemSym0

Defined in Data.Singletons.TypeLits

Methods

suppressUnusedWarnings :: ()

type Apply RemSym0 (a6989586621679478572 :: Nat)

Defined in Data.Singletons.TypeLits

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

data RemSym1 (a6989586621679478572 :: Nat) :: (~>) Nat Nat infixl 7

Instances

SuppressUnusedWarnings (RemSym1 a6989586621679478572 :: TyFun Nat Nat -> Type)

Defined in Data.Singletons.TypeLits

Methods

suppressUnusedWarnings :: ()

type Apply (RemSym1 a6989586621679478572 :: TyFun Nat Nat -> Type) (a6989586621679478573 :: Nat)

Defined in Data.Singletons.TypeLits

type Apply (RemSym1 a6989586621679478572 :: TyFun Nat Nat -> Type) (a6989586621679478573 :: Nat) = Rem a6989586621679478572 a6989586621679478573

type RemSym2 (a6989586621679478572 :: Nat) (a6989586621679478573 :: Nat) = Rem a6989586621679478572 a6989586621679478573

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

Instances

SuppressUnusedWarnings QuotRemSym0

Defined in Data.Singletons.TypeLits

Methods

suppressUnusedWarnings :: ()

type Apply QuotRemSym0 (a6989586621679478598 :: Nat)

Defined in Data.Singletons.TypeLits

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

data QuotRemSym1 (a6989586621679478598 :: Nat) :: (~>) Nat (Nat, Nat)

Instances

SuppressUnusedWarnings (QuotRemSym1 a6989586621679478598 :: TyFun Nat (Nat, Nat) -> Type)

Defined in Data.Singletons.TypeLits

Methods

suppressUnusedWarnings :: ()

type Apply (QuotRemSym1 a6989586621679478598 :: TyFun Nat (Nat, Nat) -> Type) (a6989586621679478599 :: Nat)

Defined in Data.Singletons.TypeLits

type Apply (QuotRemSym1 a6989586621679478598 :: TyFun Nat (Nat, Nat) -> Type) (a6989586621679478599 :: Nat) = QuotRem a6989586621679478598 a6989586621679478599

type QuotRemSym2 (a6989586621679478598 :: Nat) (a6989586621679478599 :: Nat) = QuotRem a6989586621679478598 a6989586621679478599

Orphan instances

Enum Nat

Methods

succ :: Nat -> Nat

pred :: Nat -> Nat

toEnum :: Int -> Nat

fromEnum :: Nat -> Int

enumFrom :: Nat -> [Nat]

enumFromThen :: Nat -> Nat -> [Nat]

enumFromTo :: Nat -> Nat -> [Nat]

enumFromThenTo :: Nat -> Nat -> Nat -> [Nat]

Eq Nat

Methods

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

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

Eq Symbol

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.

Methods

(==) :: Symbol -> Symbol -> Bool

(/=) :: Symbol -> Symbol -> Bool

Num Nat

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.

Methods

(+) :: Nat -> Nat -> Nat

(-) :: Nat -> Nat -> Nat

(*) :: Nat -> Nat -> Nat

negate :: Nat -> Nat

abs :: Nat -> Nat

signum :: Nat -> Nat

fromInteger :: Integer -> Nat

Ord Nat

Methods

compare :: Nat -> Nat -> Ordering

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

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

(>) :: Nat -> Nat -> Bool

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

max :: Nat -> Nat -> Nat

min :: Nat -> Nat -> Nat

Ord Symbol

Methods

compare :: Symbol -> Symbol -> Ordering

(<) :: Symbol -> Symbol -> Bool

(<=) :: Symbol -> Symbol -> Bool

(>) :: Symbol -> Symbol -> Bool

(>=) :: Symbol -> Symbol -> Bool

max :: Symbol -> Symbol -> Symbol

min :: Symbol -> Symbol -> Symbol

Show Nat

Methods

showsPrec :: Int -> Nat -> ShowS

show :: Nat -> String

showList :: [Nat] -> ShowS

Show Symbol

Methods

showsPrec :: Int -> Symbol -> ShowS

show :: Symbol -> String

showList :: [Symbol] -> ShowS

IsString Symbol

Methods

fromString :: String -> Symbol

Semigroup Symbol

Methods

(<>) :: Symbol -> Symbol -> Symbol

sconcat :: NonEmpty Symbol -> Symbol

stimes :: Integral b => b -> Symbol -> Symbol

Monoid Symbol

Methods

mempty :: Symbol

mappend :: Symbol -> Symbol -> Symbol

mconcat :: [Symbol] -> Symbol