Copyright	(C) 2014 Richard Eisenberg
License	BSD-style (see LICENSE)
Maintainer	Richard Eisenberg (rae@cs.brynmawr.edu)
Stability	experimental
Portability	non-portable
Safe Haskell	None
Language	Haskell2010

Data.Singletons.TypeLits

Contents

Defunctionalization symbols
Orphan instances

Description

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

Synopsis

data Nat
data Symbol
data family Sing (a :: k)
type SNat (x :: Nat) = Sing x
type SSymbol (x :: Symbol) = Sing x
withKnownNat :: Sing n -> (KnownNat n => r) -> r
withKnownSymbol :: Sing n -> (KnownSymbol n => r) -> r
type family Error (str :: k0) :: k where ...
sError :: Sing (str :: Symbol) -> a
type family Undefined :: k where ...
sUndefined :: a
class KnownNat (n :: Nat)
natVal :: KnownNat n => proxy n -> Natural
class KnownSymbol (n :: Symbol)
symbolVal :: KnownSymbol n => proxy n -> String
type family (a :: Nat) ^ (b :: Nat) :: Nat where ...
(%^) :: Sing a -> Sing b -> Sing (a ^ b)
type (<>) a b = AppendSymbol a b
(%<>) :: Sing a -> Sing b -> Sing (a <> b)
type family Log2 (a :: Nat) :: Nat where ...
sLog2 :: Sing x -> Sing (Log2 x)
type family Div (a :: Nat) (b :: Nat) :: Nat where ...
sDiv :: Sing x -> Sing y -> Sing (Div x y)
type family Mod (a :: Nat) (b :: Nat) :: Nat where ...
sMod :: Sing x -> Sing y -> Sing (Mod x y)
type family DivMod (a :: Nat) (a :: Nat) :: (Nat, Nat) where ...
sDivMod :: Sing x -> Sing y -> Sing (DivMod x y)
type family Quot (a :: Nat) (a :: Nat) :: Nat where ...
sQuot :: Sing x -> Sing y -> Sing (Quot x y)
type family Rem (a :: Nat) (a :: Nat) :: Nat where ...
sRem :: Sing x -> Sing y -> Sing (Rem x y)
type family QuotRem (a :: Nat) (a :: Nat) :: (Nat, Nat) where ...
sQuotRem :: Sing x -> Sing y -> Sing (QuotRem x y)
data ErrorSym0 (l :: TyFun k06989586621679403140 k6989586621679403141)
type ErrorSym1 (t :: k06989586621679403140) = Error t
type UndefinedSym0 = Undefined
data KnownNatSym0 (l :: TyFun Nat Constraint)
type KnownNatSym1 (t :: Nat) = KnownNat t
data KnownSymbolSym0 (l :: TyFun Symbol Constraint)
type KnownSymbolSym1 (t :: Symbol) = KnownSymbol t
data (^@#@$) (l :: TyFun Nat (TyFun Nat Nat -> Type))
data (l :: Nat) ^@#@$$ (l :: TyFun Nat Nat)
type (^@#@$$$) (t :: Nat) (t :: Nat) = (^) t t
data (<>@#@$) l
data (l :: Symbol) <>@#@$$ l
type (<>@#@$$$) (t :: Symbol) (t :: Symbol) = (<>) t t
data Log2Sym0 (l :: TyFun Nat Nat)
type Log2Sym1 (t :: Nat) = Log2 t
data DivSym0 (l :: TyFun Nat (TyFun Nat Nat -> Type))
data DivSym1 (l :: Nat) (l :: TyFun Nat Nat)
type DivSym2 (t :: Nat) (t :: Nat) = Div t t
data ModSym0 (l :: TyFun Nat (TyFun Nat Nat -> Type))
data ModSym1 (l :: Nat) (l :: TyFun Nat Nat)
type ModSym2 (t :: Nat) (t :: Nat) = Mod t t
data DivModSym0 (l :: TyFun Nat (TyFun Nat (Nat, Nat) -> Type))
data DivModSym1 (l :: Nat) (l :: TyFun Nat (Nat, Nat))
type DivModSym2 (t :: Nat) (t :: Nat) = DivMod t t
data QuotSym0 (l :: TyFun Nat (TyFun Nat Nat -> Type))
data QuotSym1 (l :: Nat) (l :: TyFun Nat Nat)
type QuotSym2 (t :: Nat) (t :: Nat) = Quot t t
data RemSym0 (l :: TyFun Nat (TyFun Nat Nat -> Type))
data RemSym1 (l :: Nat) (l :: TyFun Nat Nat)
type RemSym2 (t :: Nat) (t :: Nat) = Rem t t
data QuotRemSym0 (l :: TyFun Nat (TyFun Nat (Nat, Nat) -> Type))
data QuotRemSym1 (l :: Nat) (l :: TyFun Nat (Nat, Nat))
type QuotRemSym2 (t :: Nat) (t :: Nat) = QuotRem t t

Documentation

data Nat #

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

Instances

Eq Nat #
Instance details 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.
Instance details 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 #
Instance details 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 #
SingKind Nat Source #
Instance details Defined in Data.Singletons.TypeLits.Internal Associated Types type Demote Nat = (r :: *) Source # Methods fromSing :: Sing a -> Demote Nat Source # toSing :: Demote Nat -> SomeSing Nat Source #
SDecide Nat Source #
Instance details Defined in Data.Singletons.TypeLits.Internal Methods (%~) :: Sing a -> Sing b -> Decision (a :~: b) Source #
PEq Nat Source #
Instance details Defined in Data.Singletons.TypeLits.Internal Associated Types type x == y :: Bool Source # type x /= y :: Bool Source #
SEq Nat Source #
Instance details Defined in Data.Singletons.TypeLits.Internal Methods (%==) :: Sing a -> Sing b -> Sing (a == b) Source # (%/=) :: Sing a -> Sing b -> Sing (a /= b) Source #
SOrd Nat Source #
Instance details Defined in Data.Singletons.TypeLits.Internal Methods sCompare :: Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source # (%<) :: Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source # (%<=) :: Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source # (%>) :: Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source # (%>=) :: Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source # sMax :: Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source # sMin :: Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source #
POrd Nat Source #
Instance details Defined in Data.Singletons.TypeLits.Internal Associated Types type Compare arg arg :: Ordering Source # type arg < arg :: Bool Source # type arg <= arg :: Bool Source # type arg > arg :: Bool Source # type arg >= arg :: Bool Source # type Max arg arg :: a Source # type Min arg arg :: a Source #
ShowSing Nat Source #
Instance details Defined in Data.Singletons.ShowSing Methods showsSingPrec :: Int -> Sing a -> ShowS Source #
SNum Nat Source #
Instance details Defined in Data.Singletons.Prelude.Num Methods (%+) :: Sing t -> Sing t -> Sing (Apply (Apply (+@#@$) t) t) Source # (%-) :: Sing t -> Sing t -> Sing (Apply (Apply (-@#@$) t) t) Source # (%) :: Sing t -> Sing t -> Sing (Apply (Apply (@#@$) t) t) Source # sNegate :: Sing t -> Sing (Apply NegateSym0 t) Source # sAbs :: Sing t -> Sing (Apply AbsSym0 t) Source # sSignum :: Sing t -> Sing (Apply SignumSym0 t) Source # sFromInteger :: Sing t -> Sing (Apply FromIntegerSym0 t) Source #
PNum Nat Source #
Instance details Defined in Data.Singletons.Prelude.Num Associated Types type arg + arg :: a Source # type arg - arg :: a Source # type arg * arg :: a Source # type Negate arg :: a Source # type Abs arg :: a Source # type Signum arg :: a Source # type FromInteger arg :: a Source #
SShow Nat Source #
Instance details Defined in Data.Singletons.Prelude.Show Methods sShowsPrec :: Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply ShowsPrecSym0 t) t) t) Source # sShow_ :: Sing t -> Sing (Apply Show_Sym0 t) Source # sShowList :: Sing t -> Sing t -> Sing (Apply (Apply ShowListSym0 t) t) Source #
PShow Nat Source #	Note that this instance is really, really slow, since it uses an inefficient, inductive definition of division behind the hood.
Instance details Defined in Data.Singletons.Prelude.Show Associated Types type ShowsPrec arg arg arg :: Symbol Source # type Show_ arg :: Symbol Source # type ShowList arg arg :: Symbol Source #
SEnum Nat Source #
Instance details Defined in Data.Singletons.Prelude.Enum Methods sSucc :: Sing t -> Sing (Apply SuccSym0 t) Source # sPred :: Sing t -> Sing (Apply PredSym0 t) Source # sToEnum :: Sing t -> Sing (Apply ToEnumSym0 t) Source # sFromEnum :: Sing t -> Sing (Apply FromEnumSym0 t) Source # sEnumFromTo :: Sing t -> Sing t -> Sing (Apply (Apply EnumFromToSym0 t) t) Source # sEnumFromThenTo :: Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply EnumFromThenToSym0 t) t) t) Source #
PEnum Nat Source #
Instance details Defined in Data.Singletons.Prelude.Enum Associated Types type Succ arg :: a Source # type Pred arg :: a Source # type ToEnum arg :: a Source # type FromEnum arg :: Nat Source # type EnumFromTo arg arg :: [a] Source # type EnumFromThenTo arg arg arg :: [a] Source #
KnownNat n => SingI (n :: Nat) Source #
Instance details Defined in Data.Singletons.TypeLits.Internal Methods sing :: Sing n Source #
Show (SNat n) #
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> SNat n -> ShowS # show :: SNat n -> String # showList :: [SNat n] -> ShowS #
SuppressUnusedWarnings (^@#@$$) Source #
Instance details Defined in Data.Singletons.TypeLits.Internal Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings DivSym1 Source #
Instance details Defined in Data.Singletons.TypeLits Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings ModSym1 Source #
Instance details Defined in Data.Singletons.TypeLits Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings QuotSym1 Source #
Instance details Defined in Data.Singletons.TypeLits Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings RemSym1 Source #
Instance details Defined in Data.Singletons.TypeLits Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings QuotRemSym1 Source #
Instance details Defined in Data.Singletons.TypeLits Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings DivModSym1 Source #
Instance details Defined in Data.Singletons.TypeLits Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (^@#@$) Source #
Instance details Defined in Data.Singletons.TypeLits.Internal Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings DivSym0 Source #
Instance details Defined in Data.Singletons.TypeLits Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings ModSym0 Source #
Instance details Defined in Data.Singletons.TypeLits Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings QuotSym0 Source #
Instance details Defined in Data.Singletons.TypeLits Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings RemSym0 Source #
Instance details Defined in Data.Singletons.TypeLits Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings QuotRemSym0 Source #
Instance details Defined in Data.Singletons.TypeLits Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings DivModSym0 Source #
Instance details Defined in Data.Singletons.TypeLits Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings KnownNatSym0 Source #
Instance details Defined in Data.Singletons.TypeLits Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings Log2Sym0 Source #
Instance details Defined in Data.Singletons.TypeLits Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (FindIndicesSym1 :: (TyFun a6989586621679472947 Bool -> Type) -> TyFun [a6989586621679472947] [Nat] -> *) Source #
Instance details Defined in Data.Singletons.Prelude.List Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (FindIndexSym1 :: (TyFun a6989586621679472948 Bool -> Type) -> TyFun [a6989586621679472948] (Maybe Nat) -> *) Source #
Instance details Defined in Data.Singletons.Prelude.List Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings ((!!@#@$$) :: [a6989586621679472921] -> TyFun Nat a6989586621679472921 -> *) Source #
Instance details Defined in Data.Singletons.Prelude.List Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (ShowsPrecSym2 :: Nat -> a6989586621679729880 -> TyFun Symbol Symbol -> *) Source #
Instance details Defined in Data.Singletons.Prelude.Show Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (DropSym1 :: Nat -> TyFun [a6989586621679472938] [a6989586621679472938] -> *) Source #
Instance details Defined in Data.Singletons.Prelude.List Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (TakeSym1 :: Nat -> TyFun [a6989586621679472939] [a6989586621679472939] -> *) Source #
Instance details Defined in Data.Singletons.Prelude.List Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (SplitAtSym1 :: Nat -> TyFun [a6989586621679472937] ([a6989586621679472937], [a6989586621679472937]) -> *) Source #
Instance details Defined in Data.Singletons.Prelude.List Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (ReplicateSym1 :: Nat -> TyFun a6989586621679472923 [a6989586621679472923] -> *) Source #
Instance details Defined in Data.Singletons.Prelude.List Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (ShowsPrecSym1 :: Nat -> TyFun a6989586621679729880 (TyFun Symbol Symbol -> Type) -> *) Source #
Instance details Defined in Data.Singletons.Prelude.Show Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (TakeSym1 :: Nat -> TyFun (NonEmpty a6989586621679833998) [a6989586621679833998] -> *) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (DropSym1 :: Nat -> TyFun (NonEmpty a6989586621679833997) [a6989586621679833997] -> *) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (SplitAtSym1 :: Nat -> TyFun (NonEmpty a6989586621679833996) ([a6989586621679833996], [a6989586621679833996]) -> *) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (ElemIndicesSym1 :: a6989586621679472949 -> TyFun [a6989586621679472949] [Nat] -> *) Source #
Instance details Defined in Data.Singletons.Prelude.List Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (ElemIndexSym1 :: a6989586621679472950 -> TyFun [a6989586621679472950] (Maybe Nat) -> *) Source #
Instance details Defined in Data.Singletons.Prelude.List Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings ((!!@#@$$) :: NonEmpty a6989586621679833976 -> TyFun Nat a6989586621679833976 -> *) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (FindIndicesSym0 :: TyFun (TyFun a6989586621679472947 Bool -> Type) (TyFun [a6989586621679472947] [Nat] -> Type) -> *) Source #
Instance details Defined in Data.Singletons.Prelude.List Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (FindIndexSym0 :: TyFun (TyFun a6989586621679472948 Bool -> Type) (TyFun [a6989586621679472948] (Maybe Nat) -> Type) -> *) Source #
Instance details Defined in Data.Singletons.Prelude.List Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings ((!!@#@$) :: TyFun [a6989586621679472921] (TyFun Nat a6989586621679472921 -> Type) -> *) Source #
Instance details Defined in Data.Singletons.Prelude.List Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (LengthSym0 :: TyFun [a6989586621679472924] Nat -> *) Source #
Instance details Defined in Data.Singletons.Prelude.List Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (DropSym0 :: TyFun Nat (TyFun [a6989586621679472938] [a6989586621679472938] -> Type) -> *) Source #
Instance details Defined in Data.Singletons.Prelude.List Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (TakeSym0 :: TyFun Nat (TyFun [a6989586621679472939] [a6989586621679472939] -> Type) -> *) Source #
Instance details Defined in Data.Singletons.Prelude.List Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (SplitAtSym0 :: TyFun Nat (TyFun [a6989586621679472937] ([a6989586621679472937], [a6989586621679472937]) -> Type) -> *) Source #
Instance details Defined in Data.Singletons.Prelude.List Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (ReplicateSym0 :: TyFun Nat (TyFun a6989586621679472923 [a6989586621679472923] -> Type) -> *) Source #
Instance details Defined in Data.Singletons.Prelude.List Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (ShowsPrecSym0 :: TyFun Nat (TyFun a6989586621679729880 (TyFun Symbol Symbol -> Type) -> Type) -> *) Source #
Instance details Defined in Data.Singletons.Prelude.Show Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (TakeSym0 :: TyFun Nat (TyFun (NonEmpty a6989586621679833998) [a6989586621679833998] -> Type) -> *) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (DropSym0 :: TyFun Nat (TyFun (NonEmpty a6989586621679833997) [a6989586621679833997] -> Type) -> *) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (SplitAtSym0 :: TyFun Nat (TyFun (NonEmpty a6989586621679833996) ([a6989586621679833996], [a6989586621679833996]) -> Type) -> *) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (FromIntegerSym0 :: TyFun Nat a6989586621679440260 -> *) Source #
Instance details Defined in Data.Singletons.Prelude.Num Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (ToEnumSym0 :: TyFun Nat a6989586621679916796 -> *) Source #
Instance details Defined in Data.Singletons.Prelude.Enum Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (ElemIndicesSym0 :: TyFun a6989586621679472949 (TyFun [a6989586621679472949] [Nat] -> Type) -> *) Source #
Instance details Defined in Data.Singletons.Prelude.List Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (ElemIndexSym0 :: TyFun a6989586621679472950 (TyFun [a6989586621679472950] (Maybe Nat) -> Type) -> *) Source #
Instance details Defined in Data.Singletons.Prelude.List Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (FromEnumSym0 :: TyFun a6989586621679916796 Nat -> *) Source #
Instance details Defined in Data.Singletons.Prelude.Enum Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings ((!!@#@$) :: TyFun (NonEmpty a6989586621679833976) (TyFun Nat a6989586621679833976 -> Type) -> *) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (LengthSym0 :: TyFun (NonEmpty a6989586621679834029) Nat -> *) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods suppressUnusedWarnings :: () Source #
type Demote Nat Source #
Instance details Defined in Data.Singletons.TypeLits.Internal type Demote Nat = Natural
data Sing (n :: Nat) Source #
Instance details Defined in Data.Singletons.TypeLits.Internal data Sing (n :: Nat) where SNat :: Sing n
type Negate (a :: Nat) Source #
Instance details Defined in Data.Singletons.Prelude.Num type Negate (a :: Nat) = (Error "Cannot negate a natural number" :: Nat)
type Abs (a :: Nat) Source #
Instance details Defined in Data.Singletons.Prelude.Num type Abs (a :: Nat) = a
type Signum (a :: Nat) Source #
Instance details Defined in Data.Singletons.Prelude.Num type Signum (a :: Nat)
type FromInteger a Source #
Instance details Defined in Data.Singletons.Prelude.Num type FromInteger a = a
type Show_ (arg :: Nat) Source #
Instance details Defined in Data.Singletons.Prelude.Show type Show_ (arg :: Nat)
type Succ (a :: Nat) Source #
Instance details Defined in Data.Singletons.Prelude.Enum type Succ (a :: Nat)
type Pred (a :: Nat) Source #
Instance details Defined in Data.Singletons.Prelude.Enum type Pred (a :: Nat)
type ToEnum a Source #
Instance details Defined in Data.Singletons.Prelude.Enum type ToEnum a
type FromEnum (a :: Nat) Source #
Instance details Defined in Data.Singletons.Prelude.Enum type FromEnum (a :: Nat)
type (a :: Nat) == (b :: Nat) Source #
Instance details Defined in Data.Singletons.TypeLits.Internal type (a :: Nat) == (b :: Nat) = a == b
type (x :: Nat) /= (y :: Nat) Source #
Instance details Defined in Data.Singletons.TypeLits.Internal type (x :: Nat) /= (y :: Nat) = Not (x == y)
type Compare (a :: Nat) (b :: Nat) Source #
Instance details Defined in Data.Singletons.TypeLits.Internal type Compare (a :: Nat) (b :: Nat) = CmpNat a b
type (arg1 :: Nat) < (arg2 :: Nat) Source #
Instance details Defined in Data.Singletons.TypeLits.Internal type (arg1 :: Nat) < (arg2 :: Nat)
type (arg1 :: Nat) <= (arg2 :: Nat) Source #
Instance details Defined in Data.Singletons.TypeLits.Internal type (arg1 :: Nat) <= (arg2 :: Nat)
type (arg1 :: Nat) > (arg2 :: Nat) Source #
Instance details Defined in Data.Singletons.TypeLits.Internal type (arg1 :: Nat) > (arg2 :: Nat)
type (arg1 :: Nat) >= (arg2 :: Nat) Source #
Instance details Defined in Data.Singletons.TypeLits.Internal type (arg1 :: Nat) >= (arg2 :: Nat)
type Max (arg1 :: Nat) (arg2 :: Nat) Source #
Instance details Defined in Data.Singletons.TypeLits.Internal type Max (arg1 :: Nat) (arg2 :: Nat)
type Min (arg1 :: Nat) (arg2 :: Nat) Source #
Instance details Defined in Data.Singletons.TypeLits.Internal type Min (arg1 :: Nat) (arg2 :: Nat)
type (a :: Nat) + (b :: Nat) Source #
Instance details Defined in Data.Singletons.Prelude.Num type (a :: Nat) + (b :: Nat) = a + b
type (a :: Nat) - (b :: Nat) Source #
Instance details Defined in Data.Singletons.Prelude.Num type (a :: Nat) - (b :: Nat) = a - b
type (a :: Nat) * (b :: Nat) Source #
Instance details Defined in Data.Singletons.Prelude.Num type (a :: Nat) * (b :: Nat) = a * b
type ShowList (arg1 :: [Nat]) arg2 Source #
Instance details Defined in Data.Singletons.Prelude.Show type ShowList (arg1 :: [Nat]) arg2
type EnumFromTo (a1 :: Nat) (a2 :: Nat) Source #
Instance details Defined in Data.Singletons.Prelude.Enum type EnumFromTo (a1 :: Nat) (a2 :: Nat)
type Apply KnownNatSym0 (l :: Nat) Source #
Instance details Defined in Data.Singletons.TypeLits type Apply KnownNatSym0 (l :: Nat) = KnownNat l
type Apply Log2Sym0 (l :: Nat) Source #
Instance details Defined in Data.Singletons.TypeLits type Apply Log2Sym0 (l :: Nat) = Log2 l
type ShowsPrec _ (n :: Nat) x Source #
Instance details Defined in Data.Singletons.Prelude.Show type ShowsPrec _ (n :: Nat) x
type EnumFromThenTo (a1 :: Nat) (a2 :: Nat) (a3 :: Nat) Source #
Instance details Defined in Data.Singletons.Prelude.Enum type EnumFromThenTo (a1 :: Nat) (a2 :: Nat) (a3 :: Nat)
type Apply ((^@#@$$) l1 :: TyFun Nat Nat -> *) (l2 :: Nat) Source #
Instance details Defined in Data.Singletons.TypeLits.Internal type Apply ((^@#@$$) l1 :: TyFun Nat Nat -> *) (l2 :: Nat) = l1 ^ l2
type Apply (DivSym1 l1 :: TyFun Nat Nat -> *) (l2 :: Nat) Source #
Instance details Defined in Data.Singletons.TypeLits type Apply (DivSym1 l1 :: TyFun Nat Nat -> *) (l2 :: Nat) = Div l1 l2
type Apply (ModSym1 l1 :: TyFun Nat Nat -> *) (l2 :: Nat) Source #
Instance details Defined in Data.Singletons.TypeLits type Apply (ModSym1 l1 :: TyFun Nat Nat -> *) (l2 :: Nat) = Mod l1 l2
type Apply (QuotSym1 l1 :: TyFun Nat Nat -> *) (l2 :: Nat) Source #
Instance details Defined in Data.Singletons.TypeLits type Apply (QuotSym1 l1 :: TyFun Nat Nat -> *) (l2 :: Nat) = Quot l1 l2
type Apply (RemSym1 l1 :: TyFun Nat Nat -> *) (l2 :: Nat) Source #
Instance details Defined in Data.Singletons.TypeLits type Apply (RemSym1 l1 :: TyFun Nat Nat -> *) (l2 :: Nat) = Rem l1 l2
type Apply (FromIntegerSym0 :: TyFun Nat k2 -> *) (l :: Nat) Source #
Instance details Defined in Data.Singletons.Prelude.Num type Apply (FromIntegerSym0 :: TyFun Nat k2 -> *) (l :: Nat) = (FromInteger l :: k2)
type Apply (ToEnumSym0 :: TyFun Nat k2 -> *) (l :: Nat) Source #
Instance details Defined in Data.Singletons.Prelude.Enum type Apply (ToEnumSym0 :: TyFun Nat k2 -> *) (l :: Nat) = (ToEnum l :: k2)
type Apply (FromEnumSym0 :: TyFun a Nat -> *) (l :: a) Source #
Instance details Defined in Data.Singletons.Prelude.Enum type Apply (FromEnumSym0 :: TyFun a Nat -> *) (l :: a) = FromEnum l
type Apply ((!!@#@$$) l1 :: TyFun Nat a -> *) (l2 :: Nat) Source #
Instance details Defined in Data.Singletons.Prelude.List type Apply ((!!@#@$$) l1 :: TyFun Nat a -> *) (l2 :: Nat) = l1 !! l2
type Apply ((!!@#@$$) l1 :: TyFun Nat a -> *) (l2 :: Nat) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty type Apply ((!!@#@$$) l1 :: TyFun Nat a -> *) (l2 :: Nat) = l1 !! l2
type Apply (^@#@$) (l :: Nat) Source #
Instance details Defined in Data.Singletons.TypeLits.Internal type Apply (^@#@$) (l :: Nat) = (^@#@$$) l
type Apply DivSym0 (l :: Nat) Source #
Instance details Defined in Data.Singletons.TypeLits type Apply DivSym0 (l :: Nat) = DivSym1 l
type Apply ModSym0 (l :: Nat) Source #
Instance details Defined in Data.Singletons.TypeLits type Apply ModSym0 (l :: Nat) = ModSym1 l
type Apply QuotSym0 (l :: Nat) Source #
Instance details Defined in Data.Singletons.TypeLits type Apply QuotSym0 (l :: Nat) = QuotSym1 l
type Apply RemSym0 (l :: Nat) Source #
Instance details Defined in Data.Singletons.TypeLits type Apply RemSym0 (l :: Nat) = RemSym1 l
type Apply QuotRemSym0 (l :: Nat) Source #
Instance details Defined in Data.Singletons.TypeLits type Apply QuotRemSym0 (l :: Nat) = QuotRemSym1 l
type Apply DivModSym0 (l :: Nat) Source #
Instance details Defined in Data.Singletons.TypeLits type Apply DivModSym0 (l :: Nat) = DivModSym1 l
type Apply (DropSym0 :: TyFun Nat (TyFun [a6989586621679472938] [a6989586621679472938] -> Type) -> *) (l :: Nat) Source #
Instance details Defined in Data.Singletons.Prelude.List type Apply (DropSym0 :: TyFun Nat (TyFun [a6989586621679472938] [a6989586621679472938] -> Type) -> ) (l :: Nat) = (DropSym1 l :: TyFun [a6989586621679472938] [a6989586621679472938] -> )
type Apply (TakeSym0 :: TyFun Nat (TyFun [a6989586621679472939] [a6989586621679472939] -> Type) -> *) (l :: Nat) Source #
Instance details Defined in Data.Singletons.Prelude.List type Apply (TakeSym0 :: TyFun Nat (TyFun [a6989586621679472939] [a6989586621679472939] -> Type) -> ) (l :: Nat) = (TakeSym1 l :: TyFun [a6989586621679472939] [a6989586621679472939] -> )
type Apply (SplitAtSym0 :: TyFun Nat (TyFun [a6989586621679472937] ([a6989586621679472937], [a6989586621679472937]) -> Type) -> *) (l :: Nat) Source #
Instance details Defined in Data.Singletons.Prelude.List type Apply (SplitAtSym0 :: TyFun Nat (TyFun [a6989586621679472937] ([a6989586621679472937], [a6989586621679472937]) -> Type) -> ) (l :: Nat) = (SplitAtSym1 l :: TyFun [a6989586621679472937] ([a6989586621679472937], [a6989586621679472937]) -> )
type Apply (ReplicateSym0 :: TyFun Nat (TyFun a6989586621679472923 [a6989586621679472923] -> Type) -> *) (l :: Nat) Source #
Instance details Defined in Data.Singletons.Prelude.List type Apply (ReplicateSym0 :: TyFun Nat (TyFun a6989586621679472923 [a6989586621679472923] -> Type) -> ) (l :: Nat) = (ReplicateSym1 l :: TyFun a6989586621679472923 [a6989586621679472923] -> )
type Apply (ShowsPrecSym0 :: TyFun Nat (TyFun a6989586621679729880 (TyFun Symbol Symbol -> Type) -> Type) -> *) (l :: Nat) Source #
Instance details Defined in Data.Singletons.Prelude.Show type Apply (ShowsPrecSym0 :: TyFun Nat (TyFun a6989586621679729880 (TyFun Symbol Symbol -> Type) -> Type) -> ) (l :: Nat) = (ShowsPrecSym1 l :: TyFun a6989586621679729880 (TyFun Symbol Symbol -> Type) -> )
type Apply (TakeSym0 :: TyFun Nat (TyFun (NonEmpty a6989586621679833998) [a6989586621679833998] -> Type) -> *) (l :: Nat) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty type Apply (TakeSym0 :: TyFun Nat (TyFun (NonEmpty a6989586621679833998) [a6989586621679833998] -> Type) -> ) (l :: Nat) = (TakeSym1 l :: TyFun (NonEmpty a6989586621679833998) [a6989586621679833998] -> )
type Apply (DropSym0 :: TyFun Nat (TyFun (NonEmpty a6989586621679833997) [a6989586621679833997] -> Type) -> *) (l :: Nat) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty type Apply (DropSym0 :: TyFun Nat (TyFun (NonEmpty a6989586621679833997) [a6989586621679833997] -> Type) -> ) (l :: Nat) = (DropSym1 l :: TyFun (NonEmpty a6989586621679833997) [a6989586621679833997] -> )
type Apply (SplitAtSym0 :: TyFun Nat (TyFun (NonEmpty a6989586621679833996) ([a6989586621679833996], [a6989586621679833996]) -> Type) -> *) (l :: Nat) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty type Apply (SplitAtSym0 :: TyFun Nat (TyFun (NonEmpty a6989586621679833996) ([a6989586621679833996], [a6989586621679833996]) -> Type) -> ) (l :: Nat) = (SplitAtSym1 l :: TyFun (NonEmpty a6989586621679833996) ([a6989586621679833996], [a6989586621679833996]) -> )
type Apply (QuotRemSym1 l1 :: TyFun Nat (Nat, Nat) -> *) (l2 :: Nat) Source #
Instance details Defined in Data.Singletons.TypeLits type Apply (QuotRemSym1 l1 :: TyFun Nat (Nat, Nat) -> *) (l2 :: Nat) = QuotRem l1 l2
type Apply (DivModSym1 l1 :: TyFun Nat (Nat, Nat) -> *) (l2 :: Nat) Source #
Instance details Defined in Data.Singletons.TypeLits type Apply (DivModSym1 l1 :: TyFun Nat (Nat, Nat) -> *) (l2 :: Nat) = DivMod l1 l2
type Apply (ElemIndicesSym0 :: TyFun a6989586621679472949 (TyFun [a6989586621679472949] [Nat] -> Type) -> *) (l :: a6989586621679472949) Source #
Instance details Defined in Data.Singletons.Prelude.List type Apply (ElemIndicesSym0 :: TyFun a6989586621679472949 (TyFun [a6989586621679472949] [Nat] -> Type) -> *) (l :: a6989586621679472949) = ElemIndicesSym1 l
type Apply (ElemIndexSym0 :: TyFun a6989586621679472950 (TyFun [a6989586621679472950] (Maybe Nat) -> Type) -> *) (l :: a6989586621679472950) Source #
Instance details Defined in Data.Singletons.Prelude.List type Apply (ElemIndexSym0 :: TyFun a6989586621679472950 (TyFun [a6989586621679472950] (Maybe Nat) -> Type) -> *) (l :: a6989586621679472950) = ElemIndexSym1 l
type Apply (LengthSym0 :: TyFun [a] Nat -> *) (l :: [a]) Source #
Instance details Defined in Data.Singletons.Prelude.List type Apply (LengthSym0 :: TyFun [a] Nat -> *) (l :: [a]) = Length l
type Apply (LengthSym0 :: TyFun (NonEmpty a) Nat -> *) (l :: NonEmpty a) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty type Apply (LengthSym0 :: TyFun (NonEmpty a) Nat -> *) (l :: NonEmpty a) = Length l
type Apply (FindIndicesSym1 l1 :: TyFun [a] [Nat] -> *) (l2 :: [a]) Source #
Instance details Defined in Data.Singletons.Prelude.List type Apply (FindIndicesSym1 l1 :: TyFun [a] [Nat] -> *) (l2 :: [a]) = FindIndices l1 l2
type Apply (ElemIndicesSym1 l1 :: TyFun [a] [Nat] -> *) (l2 :: [a]) Source #
Instance details Defined in Data.Singletons.Prelude.List type Apply (ElemIndicesSym1 l1 :: TyFun [a] [Nat] -> *) (l2 :: [a]) = ElemIndices l1 l2
type Apply (FindIndexSym1 l1 :: TyFun [a] (Maybe Nat) -> *) (l2 :: [a]) Source #
Instance details Defined in Data.Singletons.Prelude.List type Apply (FindIndexSym1 l1 :: TyFun [a] (Maybe Nat) -> *) (l2 :: [a]) = FindIndex l1 l2
type Apply (ElemIndexSym1 l1 :: TyFun [a] (Maybe Nat) -> *) (l2 :: [a]) Source #
Instance details Defined in Data.Singletons.Prelude.List type Apply (ElemIndexSym1 l1 :: TyFun [a] (Maybe Nat) -> *) (l2 :: [a]) = ElemIndex l1 l2
type Apply ((!!@#@$) :: TyFun [a6989586621679472921] (TyFun Nat a6989586621679472921 -> Type) -> *) (l :: [a6989586621679472921]) Source #
Instance details Defined in Data.Singletons.Prelude.List type Apply ((!!@#@$) :: TyFun [a6989586621679472921] (TyFun Nat a6989586621679472921 -> Type) -> *) (l :: [a6989586621679472921]) = (!!@#@$$) l
type Apply ((!!@#@$) :: TyFun (NonEmpty a6989586621679833976) (TyFun Nat a6989586621679833976 -> Type) -> *) (l :: NonEmpty a6989586621679833976) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty type Apply ((!!@#@$) :: TyFun (NonEmpty a6989586621679833976) (TyFun Nat a6989586621679833976 -> Type) -> *) (l :: NonEmpty a6989586621679833976) = (!!@#@$$) l
type Apply (FindIndicesSym0 :: TyFun (TyFun a6989586621679472947 Bool -> Type) (TyFun [a6989586621679472947] [Nat] -> Type) -> *) (l :: TyFun a6989586621679472947 Bool -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List type Apply (FindIndicesSym0 :: TyFun (TyFun a6989586621679472947 Bool -> Type) (TyFun [a6989586621679472947] [Nat] -> Type) -> *) (l :: TyFun a6989586621679472947 Bool -> Type) = FindIndicesSym1 l
type Apply (FindIndexSym0 :: TyFun (TyFun a6989586621679472948 Bool -> Type) (TyFun [a6989586621679472948] (Maybe Nat) -> Type) -> *) (l :: TyFun a6989586621679472948 Bool -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List type Apply (FindIndexSym0 :: TyFun (TyFun a6989586621679472948 Bool -> Type) (TyFun [a6989586621679472948] (Maybe Nat) -> Type) -> *) (l :: TyFun a6989586621679472948 Bool -> Type) = FindIndexSym1 l

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.
Instance details Defined in Data.Singletons.TypeLits Methods (==) :: Symbol -> Symbol -> Bool # (/=) :: Symbol -> Symbol -> Bool #
Ord Symbol #
Instance details 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 #
IsString Symbol #
Instance details Defined in Data.Singletons.TypeLits Methods fromString :: String -> Symbol #
SingKind Symbol	Since: base-4.9.0.0
Instance details Defined in GHC.Generics Associated Types type DemoteRep Symbol :: * Methods fromSing :: Sing a -> DemoteRep Symbol
SingKind Symbol Source #
Instance details Defined in Data.Singletons.TypeLits.Internal Associated Types type Demote Symbol = (r :: *) Source # Methods fromSing :: Sing a -> Demote Symbol Source # toSing :: Demote Symbol -> SomeSing Symbol Source #
SDecide Symbol Source #
Instance details Defined in Data.Singletons.TypeLits.Internal Methods (%~) :: Sing a -> Sing b -> Decision (a :~: b) Source #
PEq Symbol Source #
Instance details Defined in Data.Singletons.TypeLits.Internal Associated Types type x == y :: Bool Source # type x /= y :: Bool Source #
SEq Symbol Source #
Instance details Defined in Data.Singletons.TypeLits.Internal Methods (%==) :: Sing a -> Sing b -> Sing (a == b) Source # (%/=) :: Sing a -> Sing b -> Sing (a /= b) Source #
SOrd Symbol Source #
Instance details Defined in Data.Singletons.TypeLits.Internal Methods sCompare :: Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source # (%<) :: Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source # (%<=) :: Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source # (%>) :: Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source # (%>=) :: Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source # sMax :: Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source # sMin :: Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source #
POrd Symbol Source #
Instance details Defined in Data.Singletons.TypeLits.Internal Associated Types type Compare arg arg :: Ordering Source # type arg < arg :: Bool Source # type arg <= arg :: Bool Source # type arg > arg :: Bool Source # type arg >= arg :: Bool Source # type Max arg arg :: a Source # type Min arg arg :: a Source #
ShowSing Symbol Source #
Instance details Defined in Data.Singletons.ShowSing Methods showsSingPrec :: Int -> Sing a -> ShowS Source #
SIsString Symbol Source #
Instance details Defined in Data.Singletons.Prelude.IsString Methods sFromString :: Sing t -> Sing (Apply FromStringSym0 t) Source #
PIsString Symbol Source #
Instance details Defined in Data.Singletons.Prelude.IsString Associated Types type FromString arg :: a Source #
SShow Symbol Source #
Instance details Defined in Data.Singletons.Prelude.Show Methods sShowsPrec :: Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply ShowsPrecSym0 t) t) t) Source # sShow_ :: Sing t -> Sing (Apply Show_Sym0 t) Source # sShowList :: Sing t -> Sing t -> Sing (Apply (Apply ShowListSym0 t) t) Source #
PShow Symbol Source #
Instance details Defined in Data.Singletons.Prelude.Show Associated Types type ShowsPrec arg arg arg :: Symbol Source # type Show_ arg :: Symbol Source # type ShowList arg arg :: Symbol Source #
KnownSymbol a => SingI (a :: Symbol)	Since: base-4.9.0.0
Instance details Defined in GHC.Generics Methods sing :: Sing a
KnownSymbol n => SingI (n :: Symbol) Source #
Instance details Defined in Data.Singletons.TypeLits.Internal Methods sing :: Sing n Source #
Show (SSymbol s) #
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> SSymbol s -> ShowS # show :: SSymbol s -> String # showList :: [SSymbol s] -> ShowS #
SuppressUnusedWarnings ShowParenSym2 Source #
Instance details Defined in Data.Singletons.Prelude.Show Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings ShowParenSym1 Source #
Instance details Defined in Data.Singletons.Prelude.Show Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (<>@#@$$) Source #
Instance details Defined in Data.Singletons.TypeLits.Internal Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings ShowCharSym1 Source #
Instance details Defined in Data.Singletons.Prelude.Show Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings ShowStringSym1 Source #
Instance details Defined in Data.Singletons.Prelude.Show Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings ShowParenSym0 Source #
Instance details Defined in Data.Singletons.Prelude.Show Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings UnlinesSym0 Source #
Instance details Defined in Data.Singletons.Prelude.List Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings UnwordsSym0 Source #
Instance details Defined in Data.Singletons.Prelude.List Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings ShowCharSym0 Source #
Instance details Defined in Data.Singletons.Prelude.Show Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings ShowStringSym0 Source #
Instance details Defined in Data.Singletons.Prelude.Show Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (<>@#@$) Source #
Instance details Defined in Data.Singletons.TypeLits.Internal Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings KnownSymbolSym0 Source #
Instance details Defined in Data.Singletons.TypeLits Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings ShowCommaSpaceSym0 Source #
Instance details Defined in Data.Singletons.Prelude.Show Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings ShowSpaceSym0 Source #
Instance details Defined in Data.Singletons.Prelude.Show Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (ShowListWithSym2 :: (TyFun a6989586621679729864 (TyFun Symbol Symbol -> Type) -> Type) -> [a6989586621679729864] -> TyFun Symbol Symbol -> *) Source #
Instance details Defined in Data.Singletons.Prelude.Show Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (ShowListWithSym1 :: (TyFun a6989586621679729864 (TyFun Symbol Symbol -> Type) -> Type) -> TyFun [a6989586621679729864] (TyFun Symbol Symbol -> Type) -> *) Source #
Instance details Defined in Data.Singletons.Prelude.Show Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (ShowListSym1 :: [a6989586621679729880] -> TyFun Symbol Symbol -> *) Source #
Instance details Defined in Data.Singletons.Prelude.Show Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (ShowsPrecSym2 :: Nat -> a6989586621679729880 -> TyFun Symbol Symbol -> *) Source #
Instance details Defined in Data.Singletons.Prelude.Show Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (ShowsPrecSym1 :: Nat -> TyFun a6989586621679729880 (TyFun Symbol Symbol -> Type) -> *) Source #
Instance details Defined in Data.Singletons.Prelude.Show Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (ShowsSym1 :: a6989586621679729865 -> TyFun Symbol Symbol -> *) Source #
Instance details Defined in Data.Singletons.Prelude.Show Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (ShowListWithSym0 :: TyFun (TyFun a6989586621679729864 (TyFun Symbol Symbol -> Type) -> Type) (TyFun [a6989586621679729864] (TyFun Symbol Symbol -> Type) -> Type) -> *) Source #
Instance details Defined in Data.Singletons.Prelude.Show Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (ShowListSym0 :: TyFun [a6989586621679729880] (TyFun Symbol Symbol -> Type) -> *) Source #
Instance details Defined in Data.Singletons.Prelude.Show Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (ShowsPrecSym0 :: TyFun Nat (TyFun a6989586621679729880 (TyFun Symbol Symbol -> Type) -> Type) -> *) Source #
Instance details Defined in Data.Singletons.Prelude.Show Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (FromStringSym0 :: TyFun Symbol a6989586621679439496 -> *) Source #
Instance details Defined in Data.Singletons.Prelude.IsString Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (Show_Sym0 :: TyFun a6989586621679729880 Symbol -> *) Source #
Instance details Defined in Data.Singletons.Prelude.Show Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (ShowsSym0 :: TyFun a6989586621679729865 (TyFun Symbol Symbol -> Type) -> *) Source #
Instance details Defined in Data.Singletons.Prelude.Show Methods suppressUnusedWarnings :: () Source #
data Sing (s :: Symbol)
Instance details Defined in GHC.Generics data Sing (s :: Symbol) where SSym :: Sing s
type DemoteRep Symbol
Instance details Defined in GHC.Generics type DemoteRep Symbol = String
type Demote Symbol Source #
Instance details Defined in Data.Singletons.TypeLits.Internal type Demote Symbol = Text
data Sing (n :: Symbol) Source #
Instance details Defined in Data.Singletons.TypeLits.Internal data Sing (n :: Symbol) where SSym :: Sing n
type FromString a Source #
Instance details Defined in Data.Singletons.Prelude.IsString type FromString a = a
type Show_ (arg :: Symbol) Source #
Instance details Defined in Data.Singletons.Prelude.Show type Show_ (arg :: Symbol)
type (a :: Symbol) == (b :: Symbol) Source #
Instance details Defined in Data.Singletons.TypeLits.Internal type (a :: Symbol) == (b :: Symbol) = a == b
type (x :: Symbol) /= (y :: Symbol) Source #
Instance details Defined in Data.Singletons.TypeLits.Internal type (x :: Symbol) /= (y :: Symbol) = Not (x == y)
type Compare (a :: Symbol) (b :: Symbol) Source #
Instance details Defined in Data.Singletons.TypeLits.Internal type Compare (a :: Symbol) (b :: Symbol) = CmpSymbol a b
type (arg1 :: Symbol) < (arg2 :: Symbol) Source #
Instance details Defined in Data.Singletons.TypeLits.Internal type (arg1 :: Symbol) < (arg2 :: Symbol)
type (arg1 :: Symbol) <= (arg2 :: Symbol) Source #
Instance details Defined in Data.Singletons.TypeLits.Internal type (arg1 :: Symbol) <= (arg2 :: Symbol)
type (arg1 :: Symbol) > (arg2 :: Symbol) Source #
Instance details Defined in Data.Singletons.TypeLits.Internal type (arg1 :: Symbol) > (arg2 :: Symbol)
type (arg1 :: Symbol) >= (arg2 :: Symbol) Source #
Instance details Defined in Data.Singletons.TypeLits.Internal type (arg1 :: Symbol) >= (arg2 :: Symbol)
type Max (arg1 :: Symbol) (arg2 :: Symbol) Source #
Instance details Defined in Data.Singletons.TypeLits.Internal type Max (arg1 :: Symbol) (arg2 :: Symbol)
type Min (arg1 :: Symbol) (arg2 :: Symbol) Source #
Instance details Defined in Data.Singletons.TypeLits.Internal type Min (arg1 :: Symbol) (arg2 :: Symbol)
type ShowList (arg1 :: [Symbol]) arg2 Source #
Instance details Defined in Data.Singletons.Prelude.Show type ShowList (arg1 :: [Symbol]) arg2
type Apply KnownSymbolSym0 (l :: Symbol) Source #
Instance details Defined in Data.Singletons.TypeLits type Apply KnownSymbolSym0 (l :: Symbol) = KnownSymbol l
type Apply ShowCommaSpaceSym0 (l :: Symbol) Source #
Instance details Defined in Data.Singletons.Prelude.Show type Apply ShowCommaSpaceSym0 (l :: Symbol) = ShowCommaSpace l
type Apply ShowSpaceSym0 (l :: Symbol) Source #
Instance details Defined in Data.Singletons.Prelude.Show type Apply ShowSpaceSym0 (l :: Symbol) = ShowSpace l
type ShowsPrec a1 (a2 :: Symbol) a3 Source #
Instance details Defined in Data.Singletons.Prelude.Show type ShowsPrec a1 (a2 :: Symbol) a3
type Apply ((<>@#@$$) l1 :: TyFun Symbol Symbol -> *) (l2 :: Symbol) Source #
Instance details Defined in Data.Singletons.TypeLits.Internal type Apply ((<>@#@$$) l1 :: TyFun Symbol Symbol -> *) (l2 :: Symbol) = l1 <> l2
type Apply (ShowCharSym1 l1 :: TyFun Symbol Symbol -> *) (l2 :: Symbol) Source #
Instance details Defined in Data.Singletons.Prelude.Show type Apply (ShowCharSym1 l1 :: TyFun Symbol Symbol -> *) (l2 :: Symbol) = ShowChar l1 l2
type Apply (ShowStringSym1 l1 :: TyFun Symbol Symbol -> *) (l2 :: Symbol) Source #
Instance details Defined in Data.Singletons.Prelude.Show type Apply (ShowStringSym1 l1 :: TyFun Symbol Symbol -> *) (l2 :: Symbol) = ShowString l1 l2
type Apply (FromStringSym0 :: TyFun Symbol k2 -> *) (l :: Symbol) Source #
Instance details Defined in Data.Singletons.Prelude.IsString type Apply (FromStringSym0 :: TyFun Symbol k2 -> *) (l :: Symbol) = (FromString l :: k2)
type Apply (Show_Sym0 :: TyFun a Symbol -> *) (l :: a) Source #
Instance details Defined in Data.Singletons.Prelude.Show type Apply (Show_Sym0 :: TyFun a Symbol -> *) (l :: a) = Show_ l
type Apply (ShowListSym1 l1 :: TyFun Symbol Symbol -> *) (l2 :: Symbol) Source #
Instance details Defined in Data.Singletons.Prelude.Show type Apply (ShowListSym1 l1 :: TyFun Symbol Symbol -> *) (l2 :: Symbol) = ShowList l1 l2
type Apply (ShowsSym1 l1 :: TyFun Symbol Symbol -> *) (l2 :: Symbol) Source #
Instance details Defined in Data.Singletons.Prelude.Show type Apply (ShowsSym1 l1 :: TyFun Symbol Symbol -> *) (l2 :: Symbol) = Shows l1 l2
type Apply (ShowParenSym2 l1 l2 :: TyFun Symbol Symbol -> *) (l3 :: Symbol) Source #
Instance details Defined in Data.Singletons.Prelude.Show type Apply (ShowParenSym2 l1 l2 :: TyFun Symbol Symbol -> *) (l3 :: Symbol) = ShowParen l1 l2 l3
type Apply (ShowsPrecSym2 l1 l2 :: TyFun Symbol Symbol -> *) (l3 :: Symbol) Source #
Instance details Defined in Data.Singletons.Prelude.Show type Apply (ShowsPrecSym2 l1 l2 :: TyFun Symbol Symbol -> *) (l3 :: Symbol) = ShowsPrec l1 l2 l3
type Apply (ShowListWithSym2 l1 l2 :: TyFun Symbol Symbol -> *) (l3 :: Symbol) Source #
Instance details Defined in Data.Singletons.Prelude.Show type Apply (ShowListWithSym2 l1 l2 :: TyFun Symbol Symbol -> *) (l3 :: Symbol) = ShowListWith l1 l2 l3
type Apply ShowParenSym0 (l :: Bool) Source #
Instance details Defined in Data.Singletons.Prelude.Show type Apply ShowParenSym0 (l :: Bool) = ShowParenSym1 l
type Apply ShowCharSym0 (l :: Symbol) Source #
Instance details Defined in Data.Singletons.Prelude.Show type Apply ShowCharSym0 (l :: Symbol) = ShowCharSym1 l
type Apply ShowStringSym0 (l :: Symbol) Source #
Instance details Defined in Data.Singletons.Prelude.Show type Apply ShowStringSym0 (l :: Symbol) = ShowStringSym1 l
type Apply (<>@#@$) (l :: Symbol) Source #
Instance details Defined in Data.Singletons.TypeLits.Internal type Apply (<>@#@$) (l :: Symbol) = (<>@#@$$) l
type Apply (ShowsPrecSym0 :: TyFun Nat (TyFun a6989586621679729880 (TyFun Symbol Symbol -> Type) -> Type) -> *) (l :: Nat) Source #
Instance details Defined in Data.Singletons.Prelude.Show type Apply (ShowsPrecSym0 :: TyFun Nat (TyFun a6989586621679729880 (TyFun Symbol Symbol -> Type) -> Type) -> ) (l :: Nat) = (ShowsPrecSym1 l :: TyFun a6989586621679729880 (TyFun Symbol Symbol -> Type) -> )
type Apply (ShowsSym0 :: TyFun a6989586621679729865 (TyFun Symbol Symbol -> Type) -> *) (l :: a6989586621679729865) Source #
Instance details Defined in Data.Singletons.Prelude.Show type Apply (ShowsSym0 :: TyFun a6989586621679729865 (TyFun Symbol Symbol -> Type) -> *) (l :: a6989586621679729865) = ShowsSym1 l
type Apply (ShowsPrecSym1 l1 :: TyFun a6989586621679729880 (TyFun Symbol Symbol -> Type) -> *) (l2 :: a6989586621679729880) Source #
Instance details Defined in Data.Singletons.Prelude.Show type Apply (ShowsPrecSym1 l1 :: TyFun a6989586621679729880 (TyFun Symbol Symbol -> Type) -> *) (l2 :: a6989586621679729880) = ShowsPrecSym2 l1 l2
type Apply UnlinesSym0 (l :: [Symbol]) Source #
Instance details Defined in Data.Singletons.Prelude.List type Apply UnlinesSym0 (l :: [Symbol]) = Unlines l
type Apply UnwordsSym0 (l :: [Symbol]) Source #
Instance details Defined in Data.Singletons.Prelude.List type Apply UnwordsSym0 (l :: [Symbol]) = Unwords l
type Apply (ShowListSym0 :: TyFun [a6989586621679729880] (TyFun Symbol Symbol -> Type) -> *) (l :: [a6989586621679729880]) Source #
Instance details Defined in Data.Singletons.Prelude.Show type Apply (ShowListSym0 :: TyFun [a6989586621679729880] (TyFun Symbol Symbol -> Type) -> *) (l :: [a6989586621679729880]) = ShowListSym1 l
type Apply (ShowListWithSym1 l1 :: TyFun [a6989586621679729864] (TyFun Symbol Symbol -> Type) -> *) (l2 :: [a6989586621679729864]) Source #
Instance details Defined in Data.Singletons.Prelude.Show type Apply (ShowListWithSym1 l1 :: TyFun [a6989586621679729864] (TyFun Symbol Symbol -> Type) -> *) (l2 :: [a6989586621679729864]) = ShowListWithSym2 l1 l2
type Apply (ShowParenSym1 l1 :: TyFun (TyFun Symbol Symbol -> Type) (TyFun Symbol Symbol -> Type) -> *) (l2 :: TyFun Symbol Symbol -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Show type Apply (ShowParenSym1 l1 :: TyFun (TyFun Symbol Symbol -> Type) (TyFun Symbol Symbol -> Type) -> *) (l2 :: TyFun Symbol Symbol -> Type) = ShowParenSym2 l1 l2
type Apply (ShowListWithSym0 :: TyFun (TyFun a6989586621679729864 (TyFun Symbol Symbol -> Type) -> Type) (TyFun [a6989586621679729864] (TyFun Symbol Symbol -> Type) -> Type) -> *) (l :: TyFun a6989586621679729864 (TyFun Symbol Symbol -> Type) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Show type Apply (ShowListWithSym0 :: TyFun (TyFun a6989586621679729864 (TyFun Symbol Symbol -> Type) -> Type) (TyFun [a6989586621679729864] (TyFun Symbol Symbol -> Type) -> Type) -> *) (l :: TyFun a6989586621679729864 (TyFun Symbol Symbol -> Type) -> Type) = ShowListWithSym1 l

data family Sing (a :: k) Source #

The singleton kind-indexed data family.

Instances

SDecide k => TestCoercion (Sing :: k -> *) #
Instance details Defined in Data.Singletons.Decide Methods testCoercion :: Sing a -> Sing b -> Maybe (Coercion a b) #
SDecide k => TestEquality (Sing :: k -> *) #
Instance details Defined in Data.Singletons.Decide Methods testEquality :: Sing a -> Sing b -> Maybe (a :~: b) #
Show (SSymbol s) #
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> SSymbol s -> ShowS # show :: SSymbol s -> String # showList :: [SSymbol s] -> ShowS #
Show (SNat n) #
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> SNat n -> ShowS # show :: SNat n -> String # showList :: [SNat n] -> ShowS #
Eq (Sing a) #
Instance details Defined in Data.Singletons.TypeRepStar Methods (==) :: Sing a -> Sing a -> Bool # (/=) :: Sing a -> Sing a -> Bool #
Ord (Sing a) #
Instance details Defined in Data.Singletons.TypeRepStar 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) #
Instance details 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) #
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> Sing z -> ShowS # show :: Sing z -> String # showList :: [Sing z] -> ShowS #
ShowSing a => Show (Sing z) #
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> Sing z -> ShowS # show :: Sing z -> String # showList :: [Sing z] -> ShowS #
Show (Sing z) #
Instance details 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) #
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> Sing z -> ShowS # show :: Sing z -> String # showList :: [Sing z] -> ShowS #
Show (Sing a) #
Instance details Defined in Data.Singletons.TypeRepStar Methods showsPrec :: Int -> Sing a -> ShowS # show :: Sing a -> String # showList :: [Sing a] -> ShowS #
Show (Sing z) #
Instance details 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) #
Instance details 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) #
Instance details 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) #
Instance details 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) #
Instance details 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) #
Instance details 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) #
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> Sing z -> ShowS # show :: Sing z -> String # showList :: [Sing z] -> ShowS #
Show (Sing z) #
Instance details 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) #
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> Sing z -> ShowS # show :: Sing z -> String # showList :: [Sing z] -> ShowS #
data Sing (z :: Bool) Source #
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (z :: Bool) where SFalse :: Sing False STrue :: Sing True
data Sing (z :: Ordering) Source #
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (z :: Ordering) where SLT :: Sing LT SEQ :: Sing EQ SGT :: Sing GT
data Sing (a :: Type) Source #
Instance details Defined in Data.Singletons.TypeRepStar data Sing (a :: Type) = STypeRep (TypeRep a)
data Sing (n :: Nat) Source #
Instance details Defined in Data.Singletons.TypeLits.Internal data Sing (n :: Nat) where SNat :: Sing n
data Sing (n :: Symbol) Source #
Instance details Defined in Data.Singletons.TypeLits.Internal data Sing (n :: Symbol) where SSym :: Sing n
data Sing (z :: ()) Source #
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (z :: ()) where STuple0 :: Sing ()
data Sing (z :: Void) Source #
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (z :: Void)
data Sing (z :: [a]) Source #
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (z :: [a]) where SNil :: Sing ([] :: [k]) SCons :: Sing (n ': n)
data Sing (z :: Maybe a) Source #
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (z :: Maybe a) where SNothing :: Sing (Nothing :: Maybe a) SJust :: Sing (Just n)
data Sing (z :: NonEmpty a) Source #
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (z :: NonEmpty a) where (:%\|) :: Sing (n :\| n)
data Sing (z :: Either a b) Source #
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (z :: Either a b) where SLeft :: Sing (Left n :: Either a b) SRight :: Sing (Right n :: Either a b)
data Sing (z :: (a, b)) Source #
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (z :: (a, b)) where STuple2 :: Sing ((,) n n)
data Sing (f :: k1 ~> k2) Source #
Instance details Defined in Data.Singletons.Internal data Sing (f :: k1 ~> k2) = SLambda { applySing :: forall (t :: k1). Sing t -> Sing (f @@ t) }
data Sing (z :: (a, b, c)) Source #
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (z :: (a, b, c)) where STuple3 :: Sing ((,,) n n n)
data Sing (z :: (a, b, c, d)) Source #
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (z :: (a, b, c, d)) where STuple4 :: Sing ((,,,) n n n n)
data Sing (z :: (a, b, c, d, e)) Source #
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (z :: (a, b, c, d, e)) where STuple5 :: Sing ((,,,,) n n n n n)
data Sing (z :: (a, b, c, d, e, f)) Source #
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (z :: (a, b, c, d, e, f)) where STuple6 :: Sing ((,,,,,) n n n n n n)
data Sing (z :: (a, b, c, d, e, f, g)) Source #
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (z :: (a, b, c, d, e, f, g)) where STuple7 :: Sing ((,,,,,,) n n n n n n n)

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

Kind-restricted synonym for Sing for Nats

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

Kind-restricted synonym for Sing for Symbols

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

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

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

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

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

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

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

The singleton for error

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

The promotion of undefined.

sUndefined :: a Source #

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 Source #

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

type (<>) a b = AppendSymbol a b infixr 6 Source #

The promoted analogue of '(<>)' for Symbols. This uses the special AppendSymbol type family from GHC.TypeLits.

(%<>) :: Sing a -> Sing b -> Sing (a <> b) infixr 6 Source #

The singleton analogue of '(<>)' for Symbols.

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

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 Source #

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 Source #

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

Equations

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

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

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

Equations

Quot a_6989586621679423426 a_6989586621679423428 = Apply (Apply DivSym0 a_6989586621679423426) a_6989586621679423428

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

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

Equations

Rem a_6989586621679423411 a_6989586621679423413 = Apply (Apply ModSym0 a_6989586621679423411) a_6989586621679423413

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

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

Equations

QuotRem a_6989586621679423452 a_6989586621679423454 = Apply (Apply DivModSym0 a_6989586621679423452) a_6989586621679423454

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

Defunctionalization symbols

data ErrorSym0 (l :: TyFun k06989586621679403140 k6989586621679403141) Source #

Instances

SuppressUnusedWarnings (ErrorSym0 :: TyFun k06989586621679403140 k6989586621679403141 -> *) Source #
Instance details Defined in Data.Singletons.TypeLits.Internal Methods suppressUnusedWarnings :: () Source #
type Apply (ErrorSym0 :: TyFun k0 k2 -> *) (l :: k0) Source #
Instance details Defined in Data.Singletons.TypeLits.Internal type Apply (ErrorSym0 :: TyFun k0 k2 -> *) (l :: k0) = (Error l :: k2)

type ErrorSym1 (t :: k06989586621679403140) = Error t Source #

type UndefinedSym0 = Undefined Source #

data KnownNatSym0 (l :: TyFun Nat Constraint) Source #

Instances

SuppressUnusedWarnings KnownNatSym0 Source #
Instance details Defined in Data.Singletons.TypeLits Methods suppressUnusedWarnings :: () Source #
type Apply KnownNatSym0 (l :: Nat) Source #
Instance details Defined in Data.Singletons.TypeLits type Apply KnownNatSym0 (l :: Nat) = KnownNat l

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

data KnownSymbolSym0 (l :: TyFun Symbol Constraint) Source #

Instances

SuppressUnusedWarnings KnownSymbolSym0 Source #
Instance details Defined in Data.Singletons.TypeLits Methods suppressUnusedWarnings :: () Source #
type Apply KnownSymbolSym0 (l :: Symbol) Source #
Instance details Defined in Data.Singletons.TypeLits type Apply KnownSymbolSym0 (l :: Symbol) = KnownSymbol l

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

data (^@#@$) (l :: TyFun Nat (TyFun Nat Nat -> Type)) Source #

Instances

SuppressUnusedWarnings (^@#@$) Source #
Instance details Defined in Data.Singletons.TypeLits.Internal Methods suppressUnusedWarnings :: () Source #
type Apply (^@#@$) (l :: Nat) Source #
Instance details Defined in Data.Singletons.TypeLits.Internal type Apply (^@#@$) (l :: Nat) = (^@#@$$) l

data (l :: Nat) ^@#@$$ (l :: TyFun Nat Nat) Source #

Instances

SuppressUnusedWarnings (^@#@$$) Source #
Instance details Defined in Data.Singletons.TypeLits.Internal Methods suppressUnusedWarnings :: () Source #
type Apply ((^@#@$$) l1 :: TyFun Nat Nat -> *) (l2 :: Nat) Source #
Instance details Defined in Data.Singletons.TypeLits.Internal type Apply ((^@#@$$) l1 :: TyFun Nat Nat -> *) (l2 :: Nat) = l1 ^ l2

type (^@#@$$$) (t :: Nat) (t :: Nat) = (^) t t Source #

data (<>@#@$) l Source #

Instances

SuppressUnusedWarnings (<>@#@$) Source #
Instance details Defined in Data.Singletons.TypeLits.Internal Methods suppressUnusedWarnings :: () Source #
type Apply (<>@#@$) (l :: Symbol) Source #
Instance details Defined in Data.Singletons.TypeLits.Internal type Apply (<>@#@$) (l :: Symbol) = (<>@#@$$) l

data (l :: Symbol) <>@#@$$ l Source #

Instances

SuppressUnusedWarnings (<>@#@$$) Source #
Instance details Defined in Data.Singletons.TypeLits.Internal Methods suppressUnusedWarnings :: () Source #
type Apply ((<>@#@$$) l1 :: TyFun Symbol Symbol -> *) (l2 :: Symbol) Source #
Instance details Defined in Data.Singletons.TypeLits.Internal type Apply ((<>@#@$$) l1 :: TyFun Symbol Symbol -> *) (l2 :: Symbol) = l1 <> l2

type (<>@#@$$$) (t :: Symbol) (t :: Symbol) = (<>) t t Source #

data Log2Sym0 (l :: TyFun Nat Nat) Source #

Instances

SuppressUnusedWarnings Log2Sym0 Source #
Instance details Defined in Data.Singletons.TypeLits Methods suppressUnusedWarnings :: () Source #
type Apply Log2Sym0 (l :: Nat) Source #
Instance details Defined in Data.Singletons.TypeLits type Apply Log2Sym0 (l :: Nat) = Log2 l

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

data DivSym0 (l :: TyFun Nat (TyFun Nat Nat -> Type)) Source #

Instances

SuppressUnusedWarnings DivSym0 Source #
Instance details Defined in Data.Singletons.TypeLits Methods suppressUnusedWarnings :: () Source #
type Apply DivSym0 (l :: Nat) Source #
Instance details Defined in Data.Singletons.TypeLits type Apply DivSym0 (l :: Nat) = DivSym1 l

data DivSym1 (l :: Nat) (l :: TyFun Nat Nat) Source #

Instances

SuppressUnusedWarnings DivSym1 Source #
Instance details Defined in Data.Singletons.TypeLits Methods suppressUnusedWarnings :: () Source #
type Apply (DivSym1 l1 :: TyFun Nat Nat -> *) (l2 :: Nat) Source #
Instance details Defined in Data.Singletons.TypeLits type Apply (DivSym1 l1 :: TyFun Nat Nat -> *) (l2 :: Nat) = Div l1 l2

type DivSym2 (t :: Nat) (t :: Nat) = Div t t Source #

data ModSym0 (l :: TyFun Nat (TyFun Nat Nat -> Type)) Source #

Instances

SuppressUnusedWarnings ModSym0 Source #
Instance details Defined in Data.Singletons.TypeLits Methods suppressUnusedWarnings :: () Source #
type Apply ModSym0 (l :: Nat) Source #
Instance details Defined in Data.Singletons.TypeLits type Apply ModSym0 (l :: Nat) = ModSym1 l

data ModSym1 (l :: Nat) (l :: TyFun Nat Nat) Source #

Instances

SuppressUnusedWarnings ModSym1 Source #
Instance details Defined in Data.Singletons.TypeLits Methods suppressUnusedWarnings :: () Source #
type Apply (ModSym1 l1 :: TyFun Nat Nat -> *) (l2 :: Nat) Source #
Instance details Defined in Data.Singletons.TypeLits type Apply (ModSym1 l1 :: TyFun Nat Nat -> *) (l2 :: Nat) = Mod l1 l2

type ModSym2 (t :: Nat) (t :: Nat) = Mod t t Source #

data DivModSym0 (l :: TyFun Nat (TyFun Nat (Nat, Nat) -> Type)) Source #

Instances

SuppressUnusedWarnings DivModSym0 Source #
Instance details Defined in Data.Singletons.TypeLits Methods suppressUnusedWarnings :: () Source #
type Apply DivModSym0 (l :: Nat) Source #
Instance details Defined in Data.Singletons.TypeLits type Apply DivModSym0 (l :: Nat) = DivModSym1 l

data DivModSym1 (l :: Nat) (l :: TyFun Nat (Nat, Nat)) Source #

Instances

SuppressUnusedWarnings DivModSym1 Source #
Instance details Defined in Data.Singletons.TypeLits Methods suppressUnusedWarnings :: () Source #
type Apply (DivModSym1 l1 :: TyFun Nat (Nat, Nat) -> *) (l2 :: Nat) Source #
Instance details Defined in Data.Singletons.TypeLits type Apply (DivModSym1 l1 :: TyFun Nat (Nat, Nat) -> *) (l2 :: Nat) = DivMod l1 l2

type DivModSym2 (t :: Nat) (t :: Nat) = DivMod t t Source #

data QuotSym0 (l :: TyFun Nat (TyFun Nat Nat -> Type)) Source #

Instances

SuppressUnusedWarnings QuotSym0 Source #
Instance details Defined in Data.Singletons.TypeLits Methods suppressUnusedWarnings :: () Source #
type Apply QuotSym0 (l :: Nat) Source #
Instance details Defined in Data.Singletons.TypeLits type Apply QuotSym0 (l :: Nat) = QuotSym1 l

data QuotSym1 (l :: Nat) (l :: TyFun Nat Nat) Source #

Instances

SuppressUnusedWarnings QuotSym1 Source #
Instance details Defined in Data.Singletons.TypeLits Methods suppressUnusedWarnings :: () Source #
type Apply (QuotSym1 l1 :: TyFun Nat Nat -> *) (l2 :: Nat) Source #
Instance details Defined in Data.Singletons.TypeLits type Apply (QuotSym1 l1 :: TyFun Nat Nat -> *) (l2 :: Nat) = Quot l1 l2

type QuotSym2 (t :: Nat) (t :: Nat) = Quot t t Source #

data RemSym0 (l :: TyFun Nat (TyFun Nat Nat -> Type)) Source #

Instances

SuppressUnusedWarnings RemSym0 Source #
Instance details Defined in Data.Singletons.TypeLits Methods suppressUnusedWarnings :: () Source #
type Apply RemSym0 (l :: Nat) Source #
Instance details Defined in Data.Singletons.TypeLits type Apply RemSym0 (l :: Nat) = RemSym1 l

data RemSym1 (l :: Nat) (l :: TyFun Nat Nat) Source #

Instances

SuppressUnusedWarnings RemSym1 Source #
Instance details Defined in Data.Singletons.TypeLits Methods suppressUnusedWarnings :: () Source #
type Apply (RemSym1 l1 :: TyFun Nat Nat -> *) (l2 :: Nat) Source #
Instance details Defined in Data.Singletons.TypeLits type Apply (RemSym1 l1 :: TyFun Nat Nat -> *) (l2 :: Nat) = Rem l1 l2

type RemSym2 (t :: Nat) (t :: Nat) = Rem t t Source #

data QuotRemSym0 (l :: TyFun Nat (TyFun Nat (Nat, Nat) -> Type)) Source #

Instances

SuppressUnusedWarnings QuotRemSym0 Source #
Instance details Defined in Data.Singletons.TypeLits Methods suppressUnusedWarnings :: () Source #
type Apply QuotRemSym0 (l :: Nat) Source #
Instance details Defined in Data.Singletons.TypeLits type Apply QuotRemSym0 (l :: Nat) = QuotRemSym1 l

data QuotRemSym1 (l :: Nat) (l :: TyFun Nat (Nat, Nat)) Source #

Instances

SuppressUnusedWarnings QuotRemSym1 Source #
Instance details Defined in Data.Singletons.TypeLits Methods suppressUnusedWarnings :: () Source #
type Apply (QuotRemSym1 l1 :: TyFun Nat (Nat, Nat) -> *) (l2 :: Nat) Source #
Instance details Defined in Data.Singletons.TypeLits type Apply (QuotRemSym1 l1 :: TyFun Nat (Nat, Nat) -> *) (l2 :: Nat) = QuotRem l1 l2

type QuotRemSym2 (t :: Nat) (t :: Nat) = QuotRem t t Source #

Orphan instances

Eq Nat Source #
Instance details Methods (==) :: Nat -> Nat -> Bool # (/=) :: Nat -> Nat -> Bool #
Eq Symbol Source #	This bogus instance is helpful for people who want to define functions over Symbols that will only be used at the type level or as singletons.
Instance details Methods (==) :: Symbol -> Symbol -> Bool # (/=) :: Symbol -> Symbol -> Bool #
Num Nat Source #	This bogus `Num` instance is helpful for people who want to define functions over Nats that will only be used at the type level or as singletons. A correct SNum instance for Nat singletons exists.
Instance details Methods (+) :: Nat -> Nat -> Nat # (-) :: Nat -> Nat -> Nat # (*) :: Nat -> Nat -> Nat # negate :: Nat -> Nat # abs :: Nat -> Nat # signum :: Nat -> Nat # fromInteger :: Integer -> Nat #
Ord Nat Source #
Instance details 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 Source #
Instance details 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 #
IsString Symbol Source #
Instance details Methods fromString :: String -> Symbol #