singletons-2.6: A framework for generating singleton types

Copyright | (C) 2014 Richard Eisenberg
License | BSD-style (see LICENSE)
Maintainer | Ryan Scott
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
- type family Sing :: k -> Type
- data SNat (n :: Nat) = KnownNat n => SNat
- data SSymbol (n :: Symbol) = KnownSymbol n => SSym
- withKnownNat :: Sing n -> (KnownNat n => r) -> r
- withKnownSymbol :: Sing n -> (KnownSymbol n => r) -> r
- type family Error (str :: k0) :: k where ...
- sError :: HasCallStack => Sing (str :: Symbol) -> a
- type family ErrorWithoutStackTrace (str :: k0) :: k where ...
- sErrorWithoutStackTrace :: Sing (str :: Symbol) -> a
- type family Undefined :: k where ...
- sUndefined :: HasCallStack => a
- class KnownNat (n :: Nat)
- natVal :: forall (n :: Nat) proxy. KnownNat n => proxy n -> Natural
- class KnownSymbol (n :: Symbol)
- symbolVal :: forall (n :: Symbol) proxy. KnownSymbol n => proxy n -> String
- type family (a :: Nat) ^ (b :: Nat) :: Nat where ...
- (%^) :: Sing a -> Sing b -> Sing (a ^ b)
- type family (a :: Nat) <=? (b :: Nat) :: Bool where ...
- (%<=?) :: 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 :: forall k06989586621679481929 k6989586621679481930. (~>) k06989586621679481929 k6989586621679481930
- type ErrorSym1 (str6989586621679481931 :: k06989586621679481929) = Error str6989586621679481931
- data ErrorWithoutStackTraceSym0 :: forall k06989586621679483019 k6989586621679483020. (~>) k06989586621679483019 k6989586621679483020
- type ErrorWithoutStackTraceSym1 (str6989586621679483021 :: k06989586621679483019) = ErrorWithoutStackTrace str6989586621679483021
- type UndefinedSym0 = Undefined
- data KnownNatSym0 :: (~>) Nat Constraint
- type KnownNatSym1 (n6989586621679482086 :: Nat) = KnownNat n6989586621679482086
- data KnownSymbolSym0 :: (~>) Symbol Constraint
- type KnownSymbolSym1 (n6989586621679482152 :: Symbol) = KnownSymbol n6989586621679482152
- data (^@#@$) :: (~>) Nat ((~>) Nat Nat)
- data (^@#@$$) (a3530822107858468865 :: Nat) :: (~>) Nat Nat
- type (^@#@$$$) (a3530822107858468865 :: Nat) (b3530822107858468866 :: Nat) = (^) a3530822107858468865 b3530822107858468866
- data (<=?@#@$) :: (~>) Nat ((~>) Nat Bool)
- data (<=?@#@$$) (a3530822107858468865 :: Nat) :: (~>) Nat Bool
- type (<=?@#@$$$) (a3530822107858468865 :: Nat) (b3530822107858468866 :: Nat) = (<=?) a3530822107858468865 b3530822107858468866
- data Log2Sym0 :: (~>) Nat Nat
- type Log2Sym1 (a3530822107858468865 :: Nat) = Log2 a3530822107858468865
- data DivSym0 :: (~>) Nat ((~>) Nat Nat)
- data DivSym1 (a3530822107858468865 :: Nat) :: (~>) Nat Nat
- type DivSym2 (a3530822107858468865 :: Nat) (b3530822107858468866 :: Nat) = Div a3530822107858468865 b3530822107858468866
- data ModSym0 :: (~>) Nat ((~>) Nat Nat)
- data ModSym1 (a3530822107858468865 :: Nat) :: (~>) Nat Nat
- type ModSym2 (a3530822107858468865 :: Nat) (b3530822107858468866 :: Nat) = Mod a3530822107858468865 b3530822107858468866
- data DivModSym0 :: (~>) Nat ((~>) Nat (Nat, Nat))
- data DivModSym1 (a6989586621679504216 :: Nat) :: (~>) Nat (Nat, Nat)
- type DivModSym2 (a6989586621679504216 :: Nat) (a6989586621679504217 :: Nat) = DivMod a6989586621679504216 a6989586621679504217
- data QuotSym0 :: (~>) Nat ((~>) Nat Nat)
- data QuotSym1 (a6989586621679504200 :: Nat) :: (~>) Nat Nat
- type QuotSym2 (a6989586621679504200 :: Nat) (a6989586621679504201 :: Nat) = Quot a6989586621679504200 a6989586621679504201
- data RemSym0 :: (~>) Nat ((~>) Nat Nat)
- data RemSym1 (a6989586621679504190 :: Nat) :: (~>) Nat Nat
- type RemSym2 (a6989586621679504190 :: Nat) (a6989586621679504191 :: Nat) = Rem a6989586621679504190 a6989586621679504191
- data QuotRemSym0 :: (~>) Nat ((~>) Nat (Nat, Nat))
- data QuotRemSym1 (a6989586621679504210 :: Nat) :: (~>) Nat (Nat, Nat)
- type QuotRemSym2 (a6989586621679504210 :: Nat) (a6989586621679504211 :: Nat) = QuotRem a6989586621679504210 a6989586621679504211

# Documentation

data Nat #

#### Instances

Instances details

Enum Nat |
Instance details 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 |
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
Show Nat |
Instance details Defined in Data.Singletons.TypeLits Methods showsPrec :: Int -> Nat -> ShowS show :: Nat -> String showList :: [Nat] -> ShowS
SingKind Nat Source # |
Instance details Defined in Data.Singletons.TypeLits.Internal Associated Types type Demote Nat = (r :: Type) Source # Methods fromSing :: forall (a :: Nat). Sing a -> Demote Nat Source # toSing :: Demote Nat -> SomeSing Nat Source #
SDecide Nat Source # |
Instance details Defined in Data.Singletons.TypeLits.Internal Methods (%~) :: forall (a :: Nat) (b :: Nat). 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 (%==) :: forall (a :: Nat) (b :: Nat). Sing a -> Sing b -> Sing (a == b) Source # (%/=) :: forall (a :: Nat) (b :: Nat). Sing a -> Sing b -> Sing (a /= b) Source #
SOrd Nat Source # |

Instance details

Defined in Data.Singletons.TypeLits.Internal

Methods

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

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

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

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

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

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

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

POrd Nat Source # |
Instance details Defined in Data.Singletons.TypeLits.Internal Associated Types type Compare arg arg :: Ordering Source # type arg < arg :: Bool Source # type arg <= arg :: Bool Source # type arg > arg :: Bool Source # type arg >= arg :: Bool Source # type Max arg arg :: a Source # type Min arg arg :: a Source #
SNum Nat Source # |

Instance details

Defined in Data.Singletons.Prelude.Num

Methods

(%+) :: forall (t :: Nat) (t :: Nat). Sing t -> Sing t -> Sing (Apply (Apply (+@#@$) t) t) Source #

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

(%*) :: forall (t :: Nat) (t :: Nat). Sing t -> Sing t -> Sing (Apply (Apply (*@#@$) t) t) Source #

sNegate :: forall (t :: Nat). Sing t -> Sing (Apply NegateSym0 t) Source #

sAbs :: forall (t :: Nat). Sing t -> Sing (Apply AbsSym0 t) Source #

sSignum :: forall (t :: Nat). Sing t -> Sing (Apply SignumSym0 t) Source #

sFromInteger :: forall (t :: Nat). 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 #
SEnum Nat Source # |

Instance details

Defined in Data.Singletons.Prelude.Enum

Methods

sSucc :: forall (t :: Nat). Sing t -> Sing (Apply SuccSym0 t) Source #

sPred :: forall (t :: Nat). Sing t -> Sing (Apply PredSym0 t) Source #

sToEnum :: forall (t :: Nat). Sing t -> Sing (Apply ToEnumSym0 t) Source #

sFromEnum :: forall (t :: Nat). Sing t -> Sing (Apply FromEnumSym0 t) Source #

sEnumFromTo :: forall (t :: Nat) (t :: Nat). Sing t -> Sing t -> Sing (Apply (Apply EnumFromToSym0 t) t) Source #

sEnumFromThenTo :: forall (t :: Nat) (t :: Nat) (t :: Nat). 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 #
SShow Nat Source # |
Instance details Defined in Data.Singletons.Prelude.Show Methods sShowsPrec :: forall (t :: Nat) (t :: Nat) (t :: Symbol). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply ShowsPrecSym0 t) t) t) Source # sShow_ :: forall (t :: Nat). Sing t -> Sing (Apply Show_Sym0 t) Source # sShowList :: forall (t :: [Nat]) (t :: Symbol). Sing t -> Sing t -> Sing (Apply (Apply ShowListSym0 t) t) Source #
PShow Nat Source # |
Instance details Defined in Data.Singletons.Prelude.Show Associated Types type ShowsPrec arg arg arg :: Symbol Source # type Show_ arg :: Symbol Source # type ShowList arg arg :: Symbol Source #
KnownNat n => SingI (n :: Nat) Source # |
Instance details Defined in Data.Singletons.TypeLits.Internal Methods sing :: Sing n Source #
SingI Log2Sym0 Source # |
Instance details Defined in Data.Singletons.TypeLits Methods sing :: Sing Log2Sym0 Source #
SingI (<=?@#@$) Source # |
Instance details Defined in Data.Singletons.TypeLits.Internal Methods sing :: Sing (<=?@#@$) Source #
SingI (^@#@$) Source # |
Instance details Defined in Data.Singletons.TypeLits.Internal Methods sing :: Sing (^@#@$) Source #
SingI DivSym0 Source # |
Instance details Defined in Data.Singletons.TypeLits Methods sing :: Sing DivSym0 Source #
SingI ModSym0 Source # |
Instance details Defined in Data.Singletons.TypeLits Methods sing :: Sing ModSym0 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 (<=?@#@$) Source # |
Instance details Defined in Data.Singletons.TypeLits.Internal 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 DivModSym0 Source # |
Instance details Defined in Data.Singletons.TypeLits Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings QuotRemSym0 Source # |
Instance details Defined in Data.Singletons.TypeLits Methods suppressUnusedWarnings :: () Source #
SingI x => SingI ((<=?@#@$$) x :: TyFun Nat Bool -> Type) Source # |
Instance details Defined in Data.Singletons.TypeLits.Internal Methods sing :: Sing ((<=?@#@$$) x) Source #
SingI x => SingI ((^@#@$$) x :: TyFun Nat Nat -> Type) Source # |
Instance details Defined in Data.Singletons.TypeLits.Internal Methods sing :: Sing ((^@#@$$) x) Source #
SingI x => SingI (DivSym1 x :: TyFun Nat Nat -> Type) Source # |
Instance details Defined in Data.Singletons.TypeLits Methods sing :: Sing (DivSym1 x) Source #
SingI x => SingI (ModSym1 x :: TyFun Nat Nat -> Type) Source # |
Instance details Defined in Data.Singletons.TypeLits Methods sing :: Sing (ModSym1 x) Source #
SingI ((!!@#@$) :: TyFun [a] (Nat ~> a) -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (!!@#@$) Source #
SNum a => SingI (FromIntegerSym0 :: TyFun Nat a -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Num Methods sing :: Sing FromIntegerSym0 Source #
SEnum a => SingI (ToEnumSym0 :: TyFun Nat a -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Enum Methods sing :: Sing ToEnumSym0 Source #
SingI (SplitAtSym0 :: TyFun Nat ([a] ~> ([a], [a])) -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing SplitAtSym0 Source #
SingI (DropSym0 :: TyFun Nat ([a] ~> [a]) -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing DropSym0 Source #
SingI (TakeSym0 :: TyFun Nat ([a] ~> [a]) -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing TakeSym0 Source #
SingI (ReplicateSym0 :: TyFun Nat (a ~> [a]) -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing ReplicateSym0 Source #
SShow a => SingI (ShowsPrecSym0 :: TyFun Nat (a ~> (Symbol ~> Symbol)) -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Show Methods sing :: Sing ShowsPrecSym0 Source #
SingI (SplitAtSym0 :: TyFun Nat (NonEmpty a ~> ([a], [a])) -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods sing :: Sing SplitAtSym0 Source #
SingI (DropSym0 :: TyFun Nat (NonEmpty a ~> [a]) -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods sing :: Sing DropSym0 Source #
SingI (TakeSym0 :: TyFun Nat (NonEmpty a ~> [a]) -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods sing :: Sing TakeSym0 Source #
SEnum a => SingI (FromEnumSym0 :: TyFun a Nat -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Enum Methods sing :: Sing FromEnumSym0 Source #
SEq a => SingI (ElemIndicesSym0 :: TyFun a ([a] ~> [Nat]) -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing ElemIndicesSym0 Source #
SEq a => SingI (ElemIndexSym0 :: TyFun a ([a] ~> Maybe Nat) -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing ElemIndexSym0 Source #
SingI ((!!@#@$) :: TyFun (NonEmpty a) (Nat ~> a) -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods sing :: Sing (!!@#@$) Source #
SingI (LengthSym0 :: TyFun (NonEmpty a) Nat -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods sing :: Sing LengthSym0 Source #
SingI (FindIndicesSym0 :: TyFun (a ~> Bool) ([a] ~> [Nat]) -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing FindIndicesSym0 Source #
SingI (FindIndexSym0 :: TyFun (a ~> Bool) ([a] ~> Maybe Nat) -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing FindIndexSym0 Source #
SuppressUnusedWarnings ((!!@#@$) :: TyFun [a6989586621679970188] (Nat ~> a6989586621679970188) -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings ((<=?@#@$$) a3530822107858468865 :: TyFun Nat Bool -> Type) Source # |
Instance details Defined in Data.Singletons.TypeLits.Internal Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings ((^@#@$$) a3530822107858468865 :: TyFun Nat Nat -> Type) Source # |
Instance details Defined in Data.Singletons.TypeLits.Internal Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (DivSym1 a3530822107858468865 :: TyFun Nat Nat -> Type) Source # |
Instance details Defined in Data.Singletons.TypeLits Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (ModSym1 a3530822107858468865 :: TyFun Nat Nat -> Type) Source # |
Instance details Defined in Data.Singletons.TypeLits Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (QuotSym1 a6989586621679504200 :: TyFun Nat Nat -> Type) Source # |
Instance details Defined in Data.Singletons.TypeLits Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (RemSym1 a6989586621679504190 :: TyFun Nat Nat -> Type) Source # |
Instance details Defined in Data.Singletons.TypeLits Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (DivModSym1 a6989586621679504216 :: TyFun Nat (Nat, Nat) -> Type) Source # |
Instance details Defined in Data.Singletons.TypeLits Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (QuotRemSym1 a6989586621679504210 :: TyFun Nat (Nat, Nat) -> Type) Source # |
Instance details Defined in Data.Singletons.TypeLits Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (FromIntegerSym0 :: TyFun Nat a6989586621679525469 -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Num Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (ToEnumSym0 :: TyFun Nat a6989586621679763161 -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Enum Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (DropSym0 :: TyFun Nat ([a6989586621679970205] ~> [a6989586621679970205]) -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (TakeSym0 :: TyFun Nat ([a6989586621679970206] ~> [a6989586621679970206]) -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (SplitAtSym0 :: TyFun Nat ([a6989586621679970204] ~> ([a6989586621679970204], [a6989586621679970204])) -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (ReplicateSym0 :: TyFun Nat (a6989586621679970190 ~> [a6989586621679970190]) -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (ShowsPrecSym0 :: TyFun Nat (a6989586621680290747 ~> (Symbol ~> Symbol)) -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Show Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (TakeSym0 :: TyFun Nat (NonEmpty a6989586621681159661 ~> [a6989586621681159661]) -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (DropSym0 :: TyFun Nat (NonEmpty a6989586621681159660 ~> [a6989586621681159660]) -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (SplitAtSym0 :: TyFun Nat (NonEmpty a6989586621681159659 ~> ([a6989586621681159659], [a6989586621681159659])) -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (FromEnumSym0 :: TyFun a6989586621679763161 Nat -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Enum Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (ElemIndicesSym0 :: TyFun a6989586621679970216 ([a6989586621679970216] ~> [Nat]) -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (ElemIndexSym0 :: TyFun a6989586621679970217 ([a6989586621679970217] ~> Maybe Nat) -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings ((!!@#@$) :: TyFun (NonEmpty a6989586621681159639) (Nat ~> a6989586621681159639) -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (LengthSym0 :: TyFun (NonEmpty a6989586621681159692) Nat -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (FindIndicesSym0 :: TyFun (a6989586621679970214 ~> Bool) ([a6989586621679970214] ~> [Nat]) -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (FindIndexSym0 :: TyFun (a6989586621679970215 ~> Bool) ([a6989586621679970215] ~> Maybe Nat) -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods suppressUnusedWarnings :: () Source #
SingI d => SingI (FindIndicesSym1 d :: TyFun [a] [Nat] -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (FindIndicesSym1 d) Source #
SingI d => SingI (FindIndexSym1 d :: TyFun [a] (Maybe Nat) -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (FindIndexSym1 d) Source #
(SEq a, SingI d) => SingI (ElemIndicesSym1 d :: TyFun [a] [Nat] -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (ElemIndicesSym1 d) Source #
(SEq a, SingI d) => SingI (ElemIndexSym1 d :: TyFun [a] (Maybe Nat) -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (ElemIndexSym1 d) Source #
SingI d => SingI ((!!@#@$$) d :: TyFun Nat a -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing ((!!@#@$$) d) Source #
SingI d => SingI ((!!@#@$$) d :: TyFun Nat a -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods sing :: Sing ((!!@#@$$) d) Source #
SApplicative m => SingI (ReplicateM_Sym0 :: TyFun Nat (m a ~> m ()) -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Monad Methods sing :: Sing ReplicateM_Sym0 Source #
SApplicative m => SingI (ReplicateMSym0 :: TyFun Nat (m a ~> m [a]) -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Monad Methods sing :: Sing ReplicateMSym0 Source #
SuppressUnusedWarnings (FindIndicesSym1 a6989586621679974716 :: TyFun [a6989586621679970214] [Nat] -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (ElemIndicesSym1 a6989586621679974750 :: TyFun [a6989586621679970216] [Nat] -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (FindIndexSym1 a6989586621679974742 :: TyFun [a6989586621679970215] (Maybe Nat) -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (ElemIndexSym1 a6989586621679974758 :: TyFun [a6989586621679970217] (Maybe Nat) -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings ((!!@#@$$) a6989586621679974335 :: TyFun Nat a6989586621679970188 -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings ((!!@#@$$) a6989586621681160999 :: TyFun Nat a6989586621681159639 -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (ReplicateM_Sym0 :: TyFun Nat (m6989586621681271012 a6989586621681271013 ~> m6989586621681271012 ()) -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Monad Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (ReplicateMSym0 :: TyFun Nat (m6989586621681271014 a6989586621681271015 ~> m6989586621681271014 [a6989586621681271015]) -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Monad Methods suppressUnusedWarnings :: () Source #
SFoldable t => SingI (LengthSym0 :: TyFun (t a) Nat -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing LengthSym0 Source #
SuppressUnusedWarnings (LengthSym0 :: TyFun (t6989586621680486628 a6989586621680486644) Nat -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Foldable Methods suppressUnusedWarnings :: () Source #
type Demote Nat Source # |
Instance details Defined in Data.Singletons.TypeLits.Internal type Demote Nat = Natural
type Sing Source # |
Instance details Defined in Data.Singletons.TypeLits.Internal type Sing = SNat
type Negate (a :: Nat) Source # |
Instance details Defined in Data.Singletons.Prelude.Num type Negate (a :: Nat) = Error "Cannot negate a natural number" :: Nat
type Abs (a :: Nat) Source # |
Instance details Defined in Data.Singletons.Prelude.Num type Abs (a :: Nat) = a
type Signum (a :: Nat) Source # |
Instance details Defined in Data.Singletons.Prelude.Num type Signum (a :: Nat)
type FromInteger a Source # |
Instance details Defined in Data.Singletons.Prelude.Num type FromInteger a = a
type Succ (a :: Nat) Source # |
Instance details Defined in Data.Singletons.Prelude.Enum type Succ (a :: Nat)
type Pred (a :: Nat) Source # |
Instance details Defined in Data.Singletons.Prelude.Enum type Pred (a :: Nat)
type ToEnum a Source # |
Instance details Defined in Data.Singletons.Prelude.Enum type ToEnum a
type FromEnum (a :: Nat) Source # |
Instance details Defined in Data.Singletons.Prelude.Enum type FromEnum (a :: Nat)
type Show_ (arg0 :: Nat) Source # |
Instance details Defined in Data.Singletons.Prelude.Show type Show_ (arg0 :: Nat)
type (x :: Nat) == (y :: Nat) Source # |
Instance details Defined in Data.Singletons.TypeLits.Internal type (x :: Nat) == (y :: Nat) = DefaultEq x y
type (x :: Nat) /= (y :: Nat) Source # |
Instance details Defined in Data.Singletons.TypeLits.Internal type (x :: Nat) /= (y :: Nat) = Not (x == y)
type Compare (a :: Nat) (b :: Nat) Source # |
Instance details Defined in Data.Singletons.TypeLits.Internal type Compare (a :: Nat) (b :: Nat) = CmpNat a b
type (arg1 :: Nat) < (arg2 :: Nat) Source # |
Instance details Defined in Data.Singletons.TypeLits.Internal type (arg1 :: Nat) < (arg2 :: Nat)
type (arg1 :: Nat) <= (arg2 :: Nat) Source # |
Instance details Defined in Data.Singletons.TypeLits.Internal type (arg1 :: Nat) <= (arg2 :: Nat)
type (arg1 :: Nat) > (arg2 :: Nat) Source # |
Instance details Defined in Data.Singletons.TypeLits.Internal type (arg1 :: Nat) > (arg2 :: Nat)
type (arg1 :: Nat) >= (arg2 :: Nat) Source # |
Instance details Defined in Data.Singletons.TypeLits.Internal type (arg1 :: Nat) >= (arg2 :: Nat)
type Max (arg1 :: Nat) (arg2 :: Nat) Source # |
Instance details Defined in Data.Singletons.TypeLits.Internal type Max (arg1 :: Nat) (arg2 :: Nat)
type Min (arg1 :: Nat) (arg2 :: Nat) Source # |
Instance details Defined in Data.Singletons.TypeLits.Internal type Min (arg1 :: Nat) (arg2 :: Nat)
type (a :: Nat) + (b :: Nat) Source # |
Instance details Defined in Data.Singletons.Prelude.Num type (a :: Nat) + (b :: Nat) = a + b
type (a :: Nat) - (b :: Nat) Source # |
Instance details Defined in Data.Singletons.Prelude.Num type (a :: Nat) - (b :: Nat) = a - b
type (a :: Nat) * (b :: Nat) Source # |
Instance details Defined in Data.Singletons.Prelude.Num type (a :: Nat) * (b :: Nat) = a * b
type EnumFromTo (a1 :: Nat) (a2 :: Nat) Source # |
Instance details Defined in Data.Singletons.Prelude.Enum type EnumFromTo (a1 :: Nat) (a2 :: Nat)
type ShowList (arg1 :: [Nat]) arg2 Source # |
Instance details Defined in Data.Singletons.Prelude.Show type ShowList (arg1 :: [Nat]) arg2
type Apply KnownNatSym0 (n6989586621679482086 :: Nat) Source # |
Instance details Defined in Data.Singletons.TypeLits type Apply KnownNatSym0 (n6989586621679482086 :: Nat) = KnownNat n6989586621679482086
type Apply Log2Sym0 (a3530822107858468865 :: Nat) Source # |
Instance details Defined in Data.Singletons.TypeLits type Apply Log2Sym0 (a3530822107858468865 :: Nat) = Log2 a3530822107858468865
type EnumFromThenTo (a1 :: Nat) (a2 :: Nat) (a3 :: Nat) Source # |
Instance details Defined in Data.Singletons.Prelude.Enum type EnumFromThenTo (a1 :: Nat) (a2 :: Nat) (a3 :: Nat)
type ShowsPrec _1 (n :: Nat) x Source # |
Instance details Defined in Data.Singletons.Prelude.Show type ShowsPrec _1 (n :: Nat) x
type Apply ((<=?@#@$$) a3530822107858468865 :: TyFun Nat Bool -> Type) (b3530822107858468866 :: Nat) Source # |
Instance details Defined in Data.Singletons.TypeLits.Internal type Apply ((<=?@#@$$) a3530822107858468865 :: TyFun Nat Bool -> Type) (b3530822107858468866 :: Nat) = a3530822107858468865 <=? b3530822107858468866
type Apply ((^@#@$$) a3530822107858468865 :: TyFun Nat Nat -> Type) (b3530822107858468866 :: Nat) Source # |
Instance details Defined in Data.Singletons.TypeLits.Internal type Apply ((^@#@$$) a3530822107858468865 :: TyFun Nat Nat -> Type) (b3530822107858468866 :: Nat) = a3530822107858468865 ^ b3530822107858468866
type Apply (DivSym1 a3530822107858468865 :: TyFun Nat Nat -> Type) (b3530822107858468866 :: Nat) Source # |
Instance details Defined in Data.Singletons.TypeLits type Apply (DivSym1 a3530822107858468865 :: TyFun Nat Nat -> Type) (b3530822107858468866 :: Nat) = Div a3530822107858468865 b3530822107858468866
type Apply (ModSym1 a3530822107858468865 :: TyFun Nat Nat -> Type) (b3530822107858468866 :: Nat) Source # |
Instance details Defined in Data.Singletons.TypeLits type Apply (ModSym1 a3530822107858468865 :: TyFun Nat Nat -> Type) (b3530822107858468866 :: Nat) = Mod a3530822107858468865 b3530822107858468866
type Apply (QuotSym1 a6989586621679504200 :: TyFun Nat Nat -> Type) (a6989586621679504201 :: Nat) Source # |
Instance details Defined in Data.Singletons.TypeLits type Apply (QuotSym1 a6989586621679504200 :: TyFun Nat Nat -> Type) (a6989586621679504201 :: Nat) = Quot a6989586621679504200 a6989586621679504201
type Apply (RemSym1 a6989586621679504190 :: TyFun Nat Nat -> Type) (a6989586621679504191 :: Nat) Source # |
Instance details Defined in Data.Singletons.TypeLits type Apply (RemSym1 a6989586621679504190 :: TyFun Nat Nat -> Type) (a6989586621679504191 :: Nat) = Rem a6989586621679504190 a6989586621679504191
type Apply (FromIntegerSym0 :: TyFun Nat k2 -> Type) (arg6989586621679525506 :: Nat) Source # |
Instance details Defined in Data.Singletons.Prelude.Num type Apply (FromIntegerSym0 :: TyFun Nat k2 -> Type) (arg6989586621679525506 :: Nat) = FromInteger arg6989586621679525506 :: k2
type Apply (ToEnumSym0 :: TyFun Nat k2 -> Type) (arg6989586621679763449 :: Nat) Source # |
Instance details Defined in Data.Singletons.Prelude.Enum type Apply (ToEnumSym0 :: TyFun Nat k2 -> Type) (arg6989586621679763449 :: Nat) = ToEnum arg6989586621679763449 :: k2
type Apply (FromEnumSym0 :: TyFun a Nat -> Type) (arg6989586621679763451 :: a) Source # |
Instance details Defined in Data.Singletons.Prelude.Enum type Apply (FromEnumSym0 :: TyFun a Nat -> Type) (arg6989586621679763451 :: a) = FromEnum arg6989586621679763451
type Apply ((!!@#@$$) a6989586621679974335 :: TyFun Nat a -> Type) (a6989586621679974336 :: Nat) Source # |
Instance details Defined in Data.Singletons.Prelude.List.Internal type Apply ((!!@#@$$) a6989586621679974335 :: TyFun Nat a -> Type) (a6989586621679974336 :: Nat) = a6989586621679974335 !! a6989586621679974336
type Apply ((!!@#@$$) a6989586621681160999 :: TyFun Nat a -> Type) (a6989586621681161000 :: Nat) Source # |
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty type Apply ((!!@#@$$) a6989586621681160999 :: TyFun Nat a -> Type) (a6989586621681161000 :: Nat) = a6989586621681160999 !! a6989586621681161000
type Apply (<=?@#@$) (a3530822107858468865 :: Nat) Source # |
Instance details Defined in Data.Singletons.TypeLits.Internal type Apply (<=?@#@$) (a3530822107858468865 :: Nat) = (<=?@#@$$) a3530822107858468865
type Apply (^@#@$) (a3530822107858468865 :: Nat) Source # |
Instance details Defined in Data.Singletons.TypeLits.Internal type Apply (^@#@$) (a3530822107858468865 :: Nat) = (^@#@$$) a3530822107858468865
type Apply DivSym0 (a3530822107858468865 :: Nat) Source # |
Instance details Defined in Data.Singletons.TypeLits type Apply DivSym0 (a3530822107858468865 :: Nat) = DivSym1 a3530822107858468865
type Apply ModSym0 (a3530822107858468865 :: Nat) Source # |
Instance details Defined in Data.Singletons.TypeLits type Apply ModSym0 (a3530822107858468865 :: Nat) = ModSym1 a3530822107858468865
type Apply QuotSym0 (a6989586621679504200 :: Nat) Source # |
Instance details Defined in Data.Singletons.TypeLits type Apply QuotSym0 (a6989586621679504200 :: Nat) = QuotSym1 a6989586621679504200
type Apply RemSym0 (a6989586621679504190 :: Nat) Source # |
Instance details Defined in Data.Singletons.TypeLits type Apply RemSym0 (a6989586621679504190 :: Nat) = RemSym1 a6989586621679504190
type Apply DivModSym0 (a6989586621679504216 :: Nat) Source # |
Instance details Defined in Data.Singletons.TypeLits type Apply DivModSym0 (a6989586621679504216 :: Nat) = DivModSym1 a6989586621679504216
type Apply QuotRemSym0 (a6989586621679504210 :: Nat) Source # |
Instance details Defined in Data.Singletons.TypeLits type Apply QuotRemSym0 (a6989586621679504210 :: Nat) = QuotRemSym1 a6989586621679504210
type Apply (DivModSym1 a6989586621679504216 :: TyFun Nat (Nat, Nat) -> Type) (a6989586621679504217 :: Nat) Source # |
Instance details Defined in Data.Singletons.TypeLits type Apply (DivModSym1 a6989586621679504216 :: TyFun Nat (Nat, Nat) -> Type) (a6989586621679504217 :: Nat) = DivMod a6989586621679504216 a6989586621679504217
type Apply (QuotRemSym1 a6989586621679504210 :: TyFun Nat (Nat, Nat) -> Type) (a6989586621679504211 :: Nat) Source # |
Instance details Defined in Data.Singletons.TypeLits type Apply (QuotRemSym1 a6989586621679504210 :: TyFun Nat (Nat, Nat) -> Type) (a6989586621679504211 :: Nat) = QuotRem a6989586621679504210 a6989586621679504211
type Apply (DropSym0 :: TyFun Nat ([a6989586621679970205] ~> [a6989586621679970205]) -> Type) (a6989586621679974502 :: Nat) Source # |
Instance details Defined in Data.Singletons.Prelude.List.Internal type Apply (DropSym0 :: TyFun Nat ([a6989586621679970205] ~> [a6989586621679970205]) -> Type) (a6989586621679974502 :: Nat) = DropSym1 a6989586621679974502 a6989586621679970205 :: TyFun [a6989586621679970205] [a6989586621679970205] -> Type
type Apply (TakeSym0 :: TyFun Nat ([a6989586621679970206] ~> [a6989586621679970206]) -> Type) (a6989586621679974516 :: Nat) Source # |
Instance details Defined in Data.Singletons.Prelude.List.Internal type Apply (TakeSym0 :: TyFun Nat ([a6989586621679970206] ~> [a6989586621679970206]) -> Type) (a6989586621679974516 :: Nat) = TakeSym1 a6989586621679974516 a6989586621679970206 :: TyFun [a6989586621679970206] [a6989586621679970206] -> Type
type Apply (SplitAtSym0 :: TyFun Nat ([a6989586621679970204] ~> ([a6989586621679970204], [a6989586621679970204])) -> Type) (a6989586621679974496 :: Nat) Source # |
Instance details Defined in Data.Singletons.Prelude.List.Internal type Apply (SplitAtSym0 :: TyFun Nat ([a6989586621679970204] ~> ([a6989586621679970204], [a6989586621679970204])) -> Type) (a6989586621679974496 :: Nat) = SplitAtSym1 a6989586621679974496 a6989586621679970204 :: TyFun [a6989586621679970204] ([a6989586621679970204], [a6989586621679970204]) -> Type
type Apply (ReplicateSym0 :: TyFun Nat (a6989586621679970190 ~> [a6989586621679970190]) -> Type) (a6989586621679974355 :: Nat) Source # |
Instance details Defined in Data.Singletons.Prelude.List.Internal type Apply (ReplicateSym0 :: TyFun Nat (a6989586621679970190 ~> [a6989586621679970190]) -> Type) (a6989586621679974355 :: Nat) = ReplicateSym1 a6989586621679974355 a6989586621679970190 :: TyFun a6989586621679970190 [a6989586621679970190] -> Type
type Apply (ShowsPrecSym0 :: TyFun Nat (a6989586621680290747 ~> (Symbol ~> Symbol)) -> Type) (arg6989586621680291185 :: Nat) Source # |
Instance details Defined in Data.Singletons.Prelude.Show type Apply (ShowsPrecSym0 :: TyFun Nat (a6989586621680290747 ~> (Symbol ~> Symbol)) -> Type) (arg6989586621680291185 :: Nat) = ShowsPrecSym1 arg6989586621680291185 a6989586621680290747 :: TyFun a6989586621680290747 (Symbol ~> Symbol) -> Type
type Apply (TakeSym0 :: TyFun Nat (NonEmpty a6989586621681159661 ~> [a6989586621681159661]) -> Type) (a6989586621681161210 :: Nat) Source # |
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty type Apply (TakeSym0 :: TyFun Nat (NonEmpty a6989586621681159661 ~> [a6989586621681159661]) -> Type) (a6989586621681161210 :: Nat) = TakeSym1 a6989586621681161210 a6989586621681159661 :: TyFun (NonEmpty a6989586621681159661) [a6989586621681159661] -> Type
type Apply (DropSym0 :: TyFun Nat (NonEmpty a6989586621681159660 ~> [a6989586621681159660]) -> Type) (a6989586621681161202 :: Nat) Source # |
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty type Apply (DropSym0 :: TyFun Nat (NonEmpty a6989586621681159660 ~> [a6989586621681159660]) -> Type) (a6989586621681161202 :: Nat) = DropSym1 a6989586621681161202 a6989586621681159660 :: TyFun (NonEmpty a6989586621681159660) [a6989586621681159660] -> Type
type Apply (SplitAtSym0 :: TyFun Nat (NonEmpty a6989586621681159659 ~> ([a6989586621681159659], [a6989586621681159659])) -> Type) (a6989586621681161194 :: Nat) Source # |
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty type Apply (SplitAtSym0 :: TyFun Nat (NonEmpty a6989586621681159659 ~> ([a6989586621681159659], [a6989586621681159659])) -> Type) (a6989586621681161194 :: Nat) = SplitAtSym1 a6989586621681161194 a6989586621681159659 :: TyFun (NonEmpty a6989586621681159659) ([a6989586621681159659], [a6989586621681159659]) -> Type
type Apply (ElemIndicesSym0 :: TyFun a6989586621679970216 ([a6989586621679970216] ~> [Nat]) -> Type) (a6989586621679974750 :: a6989586621679970216) Source # |
Instance details Defined in Data.Singletons.Prelude.List.Internal type Apply (ElemIndicesSym0 :: TyFun a6989586621679970216 ([a6989586621679970216] ~> [Nat]) -> Type) (a6989586621679974750 :: a6989586621679970216) = ElemIndicesSym1 a6989586621679974750
type Apply (ElemIndexSym0 :: TyFun a6989586621679970217 ([a6989586621679970217] ~> Maybe Nat) -> Type) (a6989586621679974758 :: a6989586621679970217) Source # |
Instance details Defined in Data.Singletons.Prelude.List.Internal type Apply (ElemIndexSym0 :: TyFun a6989586621679970217 ([a6989586621679970217] ~> Maybe Nat) -> Type) (a6989586621679974758 :: a6989586621679970217) = ElemIndexSym1 a6989586621679974758
type Apply (ReplicateM_Sym0 :: TyFun Nat (m6989586621681271012 a6989586621681271013 ~> m6989586621681271012 ()) -> Type) (a6989586621681271372 :: Nat) Source # |
Instance details Defined in Data.Singletons.Prelude.Monad type Apply (ReplicateM_Sym0 :: TyFun Nat (m6989586621681271012 a6989586621681271013 ~> m6989586621681271012 ()) -> Type) (a6989586621681271372 :: Nat) = ReplicateM_Sym1 a6989586621681271372 m6989586621681271012 a6989586621681271013 :: TyFun (m6989586621681271012 a6989586621681271013) (m6989586621681271012 ()) -> Type
type Apply (ReplicateMSym0 :: TyFun Nat (m6989586621681271014 a6989586621681271015 ~> m6989586621681271014 [a6989586621681271015]) -> Type) (a6989586621681271391 :: Nat) Source # |

Instance details

Defined in Data.Singletons.Prelude.Monad

type Apply (ReplicateMSym0 :: TyFun Nat (m6989586621681271014 a6989586621681271015 ~> m6989586621681271014 [a6989586621681271015]) -> Type) (a6989586621681271391 :: Nat) = ReplicateMSym1 a6989586621681271391 m6989586621681271014 a6989586621681271015 :: TyFun (m6989586621681271014 a6989586621681271015) (m6989586621681271014 [a6989586621681271015]) -> Type

type Apply (LengthSym0 :: TyFun (NonEmpty a) Nat -> Type) (a6989586621681161411 :: NonEmpty a) Source # |
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty type Apply (LengthSym0 :: TyFun (NonEmpty a) Nat -> Type) (a6989586621681161411 :: NonEmpty a) = Length a6989586621681161411
type Apply (LengthSym0 :: TyFun (t a) Nat -> Type) (arg6989586621680487289 :: t a) Source # |
Instance details Defined in Data.Singletons.Prelude.Foldable type Apply (LengthSym0 :: TyFun (t a) Nat -> Type) (arg6989586621680487289 :: t a) = Length arg6989586621680487289
type Apply (FindIndicesSym1 a6989586621679974716 :: TyFun [a] [Nat] -> Type) (a6989586621679974717 :: [a]) Source # |
Instance details Defined in Data.Singletons.Prelude.List.Internal type Apply (FindIndicesSym1 a6989586621679974716 :: TyFun [a] [Nat] -> Type) (a6989586621679974717 :: [a]) = FindIndices a6989586621679974716 a6989586621679974717
type Apply (ElemIndicesSym1 a6989586621679974750 :: TyFun [a] [Nat] -> Type) (a6989586621679974751 :: [a]) Source # |
Instance details Defined in Data.Singletons.Prelude.List.Internal type Apply (ElemIndicesSym1 a6989586621679974750 :: TyFun [a] [Nat] -> Type) (a6989586621679974751 :: [a]) = ElemIndices a6989586621679974750 a6989586621679974751
type Apply (FindIndexSym1 a6989586621679974742 :: TyFun [a] (Maybe Nat) -> Type) (a6989586621679974743 :: [a]) Source # |
Instance details Defined in Data.Singletons.Prelude.List.Internal type Apply (FindIndexSym1 a6989586621679974742 :: TyFun [a] (Maybe Nat) -> Type) (a6989586621679974743 :: [a]) = FindIndex a6989586621679974742 a6989586621679974743
type Apply (ElemIndexSym1 a6989586621679974758 :: TyFun [a] (Maybe Nat) -> Type) (a6989586621679974759 :: [a]) Source # |
Instance details Defined in Data.Singletons.Prelude.List.Internal type Apply (ElemIndexSym1 a6989586621679974758 :: TyFun [a] (Maybe Nat) -> Type) (a6989586621679974759 :: [a]) = ElemIndex a6989586621679974758 a6989586621679974759
type Apply ((!!@#@$) :: TyFun [a6989586621679970188] (Nat ~> a6989586621679970188) -> Type) (a6989586621679974335 :: [a6989586621679970188]) Source # |
Instance details Defined in Data.Singletons.Prelude.List.Internal type Apply ((!!@#@$) :: TyFun [a6989586621679970188] (Nat ~> a6989586621679970188) -> Type) (a6989586621679974335 :: [a6989586621679970188]) = (!!@#@$$) a6989586621679974335
type Apply ((!!@#@$) :: TyFun (NonEmpty a6989586621681159639) (Nat ~> a6989586621681159639) -> Type) (a6989586621681160999 :: NonEmpty a6989586621681159639) Source # |
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty type Apply ((!!@#@$) :: TyFun (NonEmpty a6989586621681159639) (Nat ~> a6989586621681159639) -> Type) (a6989586621681160999 :: NonEmpty a6989586621681159639) = (!!@#@$$) a6989586621681160999
type Apply (FindIndicesSym0 :: TyFun (a6989586621679970214 ~> Bool) ([a6989586621679970214] ~> [Nat]) -> Type) (a6989586621679974716 :: a6989586621679970214 ~> Bool) Source # |
Instance details Defined in Data.Singletons.Prelude.List.Internal type Apply (FindIndicesSym0 :: TyFun (a6989586621679970214 ~> Bool) ([a6989586621679970214] ~> [Nat]) -> Type) (a6989586621679974716 :: a6989586621679970214 ~> Bool) = FindIndicesSym1 a6989586621679974716
type Apply (FindIndexSym0 :: TyFun (a6989586621679970215 ~> Bool) ([a6989586621679970215] ~> Maybe Nat) -> Type) (a6989586621679974742 :: a6989586621679970215 ~> Bool) Source # |
Instance details Defined in Data.Singletons.Prelude.List.Internal type Apply (FindIndexSym0 :: TyFun (a6989586621679970215 ~> Bool) ([a6989586621679970215] ~> Maybe Nat) -> Type) (a6989586621679974742 :: a6989586621679970215 ~> Bool) = FindIndexSym1 a6989586621679974742

data Symbol #

#### Instances

Instances details

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
Show Symbol |
Instance details Defined in Data.Singletons.TypeLits Methods showsPrec :: Int -> Symbol -> ShowS show :: Symbol -> String showList :: [Symbol] -> ShowS
IsString Symbol |
Instance details Defined in Data.Singletons.TypeLits Methods fromString :: String -> Symbol
Semigroup Symbol |
Instance details Defined in Data.Singletons.TypeLits Methods (<>) :: Symbol -> Symbol -> Symbol sconcat :: NonEmpty Symbol -> Symbol stimes :: Integral b => b -> Symbol -> Symbol
Monoid Symbol |
Instance details Defined in Data.Singletons.TypeLits Methods mempty :: Symbol mappend :: Symbol -> Symbol -> Symbol mconcat :: [Symbol] -> Symbol
SingKind Symbol Source # |
Instance details Defined in Data.Singletons.TypeLits.Internal Associated Types type Demote Symbol = (r :: Type) Source # Methods fromSing :: forall (a :: Symbol). Sing a -> Demote Symbol Source # toSing :: Demote Symbol -> SomeSing Symbol Source #
SingKind PErrorMessage Source # |
Instance details Defined in Data.Singletons.TypeError Associated Types type Demote PErrorMessage = (r :: Type) Source # Methods fromSing :: forall (a :: PErrorMessage). Sing a -> Demote PErrorMessage Source # toSing :: Demote PErrorMessage -> SomeSing PErrorMessage Source #
SingKind Symbol |
Instance details Defined in GHC.Generics Associated Types type DemoteRep Symbol Methods fromSing :: forall (a :: Symbol). Sing a -> DemoteRep Symbol
SDecide Symbol Source # |
Instance details Defined in Data.Singletons.TypeLits.Internal Methods (%~) :: forall (a :: Symbol) (b :: Symbol). 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 (%==) :: forall (a :: Symbol) (b :: Symbol). Sing a -> Sing b -> Sing (a == b) Source # (%/=) :: forall (a :: Symbol) (b :: Symbol). Sing a -> Sing b -> Sing (a /= b) Source #
SOrd Symbol Source # |

Instance details

Defined in Data.Singletons.TypeLits.Internal

Methods

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

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

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

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

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

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

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

POrd Symbol Source # |
Instance details Defined in Data.Singletons.TypeLits.Internal Associated Types type Compare arg arg :: Ordering Source # type arg < arg :: Bool Source # type arg <= arg :: Bool Source # type arg > arg :: Bool Source # type arg >= arg :: Bool Source # type Max arg arg :: a Source # type Min arg arg :: a Source #
SSemigroup Symbol Source # |
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Methods (%<>) :: forall (t :: Symbol) (t :: Symbol). Sing t -> Sing t -> Sing (Apply (Apply (<>@#@$) t) t) Source # sSconcat :: forall (t :: NonEmpty Symbol). Sing t -> Sing (Apply SconcatSym0 t) Source #
PSemigroup Symbol Source # |
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Associated Types type arg <> arg :: a Source # type Sconcat arg :: a Source #
SShow Symbol Source # |

Instance details

Defined in Data.Singletons.Prelude.Show

Methods

sShowsPrec :: forall (t :: Nat) (t :: Symbol) (t :: Symbol). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply ShowsPrecSym0 t) t) t) Source #

sShow_ :: forall (t :: Symbol). Sing t -> Sing (Apply Show_Sym0 t) Source #

sShowList :: forall (t :: [Symbol]) (t :: Symbol). 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 #
SMonoid Symbol Source # |
Instance details Defined in Data.Singletons.Prelude.Monoid Methods sMempty :: Sing MemptySym0 Source # sMappend :: forall (t :: Symbol) (t :: Symbol). Sing t -> Sing t -> Sing (Apply (Apply MappendSym0 t) t) Source # sMconcat :: forall (t :: [Symbol]). Sing t -> Sing (Apply MconcatSym0 t) Source #
PMonoid Symbol Source # |
Instance details Defined in Data.Singletons.Prelude.Monoid Associated Types type Mempty :: a Source # type Mappend arg arg :: a Source # type Mconcat arg :: a Source #
SIsString Symbol Source # |
Instance details Defined in Data.Singletons.Prelude.IsString Methods sFromString :: forall (t :: Symbol). 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 #
KnownSymbol n => SingI (n :: Symbol) Source # |
Instance details Defined in Data.Singletons.TypeLits.Internal Methods sing :: Sing n Source #
KnownSymbol a => SingI (a :: Symbol) |
Instance details Defined in GHC.Generics Methods sing :: Sing a
SingI t => SingI ('Text t :: ErrorMessage' Symbol) Source # |
Instance details Defined in Data.Singletons.TypeError Methods sing :: Sing ('Text t) Source #
SingI ty => SingI ('ShowType ty :: ErrorMessage' Symbol) Source # |
Instance details Defined in Data.Singletons.TypeError Methods sing :: Sing ('ShowType ty) Source #
(SingI e1, SingI e2) => SingI (e1 :<>: e2 :: ErrorMessage' Symbol) Source # |
Instance details Defined in Data.Singletons.TypeError Methods sing :: Sing (e1 :<>: e2) Source #
(SingI e1, SingI e2) => SingI (e1 :$$: e2 :: ErrorMessage' Symbol) Source # |
Instance details Defined in Data.Singletons.TypeError Methods sing :: Sing (e1 :$$: e2) Source #
SingI ShowParenSym0 Source # |
Instance details Defined in Data.Singletons.Prelude.Show Methods sing :: Sing ShowParenSym0 Source #
SingI UnlinesSym0 Source # |
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing UnlinesSym0 Source #
SingI UnwordsSym0 Source # |
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing UnwordsSym0 Source #
SingI ShowSpaceSym0 Source # |
Instance details Defined in Data.Singletons.Prelude.Show Methods sing :: Sing ShowSpaceSym0 Source #
SingI ShowCommaSpaceSym0 Source # |
Instance details Defined in Data.Singletons.Prelude.Show Methods sing :: Sing ShowCommaSpaceSym0 Source #
SingI ShowCharSym0 Source # |
Instance details Defined in Data.Singletons.Prelude.Show Methods sing :: Sing ShowCharSym0 Source #
SingI ShowStringSym0 Source # |
Instance details Defined in Data.Singletons.Prelude.Show Methods sing :: Sing ShowStringSym0 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.Internal Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings UnwordsSym0 Source # |
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings KnownSymbolSym0 Source # |
Instance details Defined in Data.Singletons.TypeLits Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings ShowSpaceSym0 Source # |
Instance details Defined in Data.Singletons.Prelude.Show Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings ShowCommaSpaceSym0 Source # |
Instance details Defined in Data.Singletons.Prelude.Show 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 #
SingI (TypeErrorSym0 :: TyFun PErrorMessage b6989586621681327363 -> Type) Source # |
Instance details Defined in Data.Singletons.TypeError Methods sing :: Sing TypeErrorSym0 Source #
SShow a => SingI (ShowListSym0 :: TyFun [a] (Symbol ~> Symbol) -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Show Methods sing :: Sing ShowListSym0 Source #
SShow a => SingI (ShowsPrecSym0 :: TyFun Nat (a ~> (Symbol ~> Symbol)) -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Show Methods sing :: Sing ShowsPrecSym0 Source #
SingI d => SingI (ShowCharSym1 d :: TyFun Symbol Symbol -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Show Methods sing :: Sing (ShowCharSym1 d) Source #
SingI d => SingI (ShowStringSym1 d :: TyFun Symbol Symbol -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Show Methods sing :: Sing (ShowStringSym1 d) Source #
SIsString a => SingI (FromStringSym0 :: TyFun Symbol a -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.IsString Methods sing :: Sing FromStringSym0 Source #
SingI (TextSym0 :: TyFun Symbol (ErrorMessage' Symbol) -> Type) Source # |
Instance details Defined in Data.Singletons.TypeError Methods sing :: Sing TextSym0 Source #
SShow a => SingI (ShowsSym0 :: TyFun a (Symbol ~> Symbol) -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Show Methods sing :: Sing ShowsSym0 Source #
SShow a => SingI (Show_Sym0 :: TyFun a Symbol -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Show Methods sing :: Sing Show_Sym0 Source #
SingI d => SingI (ShowParenSym1 d :: TyFun (Symbol ~> Symbol) (Symbol ~> Symbol) -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Show Methods sing :: Sing (ShowParenSym1 d) Source #
SingI (ShowListWithSym0 :: TyFun (a ~> (Symbol ~> Symbol)) ([a] ~> (Symbol ~> Symbol)) -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Show Methods sing :: Sing ShowListWithSym0 Source #
SingI ((:$$:@#@$) :: TyFun (ErrorMessage' Symbol) (ErrorMessage' Symbol ~> ErrorMessage' Symbol) -> Type) Source # |
Instance details Defined in Data.Singletons.TypeError Methods sing :: Sing (:$$:@#@$) Source #
SingI ((:<>:@#@$) :: TyFun (ErrorMessage' Symbol) (ErrorMessage' Symbol ~> ErrorMessage' Symbol) -> Type) Source # |
Instance details Defined in Data.Singletons.TypeError Methods sing :: Sing (:<>:@#@$) Source #
SuppressUnusedWarnings (ShowListSym0 :: TyFun [a6989586621680290747] (Symbol ~> Symbol) -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Show Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (ShowsPrecSym0 :: TyFun Nat (a6989586621680290747 ~> (Symbol ~> Symbol)) -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Show Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (ShowCharSym1 a6989586621680291151 :: TyFun Symbol Symbol -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Show Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (ShowStringSym1 a6989586621680291141 :: TyFun Symbol Symbol -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Show Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (FromStringSym0 :: TyFun Symbol a6989586621681259525 -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.IsString Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (Show_Sym0 :: TyFun a6989586621680290747 Symbol -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Show Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (ShowsSym0 :: TyFun a6989586621680290732 (Symbol ~> Symbol) -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Show Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (ShowParenSym1 a6989586621680291123 :: TyFun (Symbol ~> Symbol) (Symbol ~> Symbol) -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Show Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (ShowListWithSym0 :: TyFun (a6989586621680290731 ~> (Symbol ~> Symbol)) ([a6989586621680290731] ~> (Symbol ~> Symbol)) -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Show Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (TypeErrorSym0 :: TyFun PErrorMessage b6989586621681327363 -> Type) Source # |
Instance details Defined in Data.Singletons.TypeError Methods suppressUnusedWarnings :: () Source #
SingI d => SingI (ShowListWithSym1 d :: TyFun [a] (Symbol ~> Symbol) -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Show Methods sing :: Sing (ShowListWithSym1 d) Source #
(SShow a, SingI d) => SingI (ShowListSym1 d :: TyFun Symbol Symbol -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Show Methods sing :: Sing (ShowListSym1 d) Source #
(SShow a, SingI d) => SingI (ShowsSym1 d :: TyFun Symbol Symbol -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Show Methods sing :: Sing (ShowsSym1 d) Source #
(SingI d1, SingI d2) => SingI (ShowParenSym2 d1 d2 :: TyFun Symbol Symbol -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Show Methods sing :: Sing (ShowParenSym2 d1 d2) Source #
SingI (ErrorSym0 :: TyFun Symbol a -> Type) Source # |
Instance details Defined in Data.Singletons.TypeLits.Internal Methods sing :: Sing ErrorSym0 Source #
SingI (ErrorWithoutStackTraceSym0 :: TyFun Symbol a -> Type) Source # |
Instance details Defined in Data.Singletons.TypeLits.Internal Methods sing :: Sing ErrorWithoutStackTraceSym0 Source #
(SShow a, SingI d) => SingI (ShowsPrecSym1 d a :: TyFun a (Symbol ~> Symbol) -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Show Methods sing :: Sing (ShowsPrecSym1 d a) Source #
SingI (ShowTypeSym0 :: TyFun t (ErrorMessage' Symbol) -> Type) Source # |
Instance details Defined in Data.Singletons.TypeError Methods sing :: Sing ShowTypeSym0 Source #
SingI x => SingI ((:$$:@#@$$) x :: TyFun (ErrorMessage' Symbol) (ErrorMessage' Symbol) -> Type) Source # |
Instance details Defined in Data.Singletons.TypeError Methods sing :: Sing ((:$$:@#@$$) x) Source #
SingI x => SingI ((:<>:@#@$$) x :: TyFun (ErrorMessage' Symbol) (ErrorMessage' Symbol) -> Type) Source # |
Instance details Defined in Data.Singletons.TypeError Methods sing :: Sing ((:<>:@#@$$) x) Source #
SuppressUnusedWarnings (ShowListWithSym1 a6989586621680291157 :: TyFun [a6989586621680290731] (Symbol ~> Symbol) -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Show Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (ShowListSym1 arg6989586621680291193 :: TyFun Symbol Symbol -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Show Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (ShowsSym1 a6989586621680291177 :: TyFun Symbol Symbol -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Show Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (ShowParenSym2 a6989586621680291124 a6989586621680291123 :: TyFun Symbol Symbol -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Show Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (ShowsPrecSym1 arg6989586621680291185 a6989586621680290747 :: TyFun a6989586621680290747 (Symbol ~> Symbol) -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Show Methods suppressUnusedWarnings :: () Source #
(SShow a, SingI d1, SingI d2) => SingI (ShowsPrecSym2 d1 d2 :: TyFun Symbol Symbol -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Show Methods sing :: Sing (ShowsPrecSym2 d1 d2) Source #
(SingI d1, SingI d2) => SingI (ShowListWithSym2 d1 d2 :: TyFun Symbol Symbol -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Show Methods sing :: Sing (ShowListWithSym2 d1 d2) Source #
SuppressUnusedWarnings (ShowsPrecSym2 arg6989586621680291186 arg6989586621680291185 :: TyFun Symbol Symbol -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Show Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (ShowListWithSym2 a6989586621680291158 a6989586621680291157 :: TyFun Symbol Symbol -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Show Methods suppressUnusedWarnings :: () Source #
type Demote Symbol Source # |
Instance details Defined in Data.Singletons.TypeLits.Internal type Demote Symbol = Text
type Demote PErrorMessage Source # |
Instance details Defined in Data.Singletons.TypeError type Demote PErrorMessage = ErrorMessage
type Sing Source # |
Instance details Defined in Data.Singletons.TypeLits.Internal type Sing = SSymbol
type Sing Source # |
Instance details Defined in Data.Singletons.TypeError type Sing = SErrorMessage
type DemoteRep Symbol |
Instance details Defined in GHC.Generics type DemoteRep Symbol = String
data Sing (s :: Symbol) |

Instance details

Defined in GHC.Generics

data Sing (s :: Symbol) where

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

type Mempty Source # |
Instance details Defined in Data.Singletons.Prelude.Monoid type Mempty
type Sconcat (arg0 :: NonEmpty Symbol) Source # |
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type Sconcat (arg0 :: NonEmpty Symbol)
type Show_ (arg0 :: Symbol) Source # |
Instance details Defined in Data.Singletons.Prelude.Show type Show_ (arg0 :: Symbol)
type Mconcat (arg0 :: [Symbol]) Source # |
Instance details Defined in Data.Singletons.Prelude.Monoid type Mconcat (arg0 :: [Symbol])
type FromString a Source # |
Instance details Defined in Data.Singletons.Prelude.IsString type FromString a = a
type (x :: Symbol) == (y :: Symbol) Source # |
Instance details Defined in Data.Singletons.TypeLits.Internal type (x :: Symbol) == (y :: Symbol) = DefaultEq x y
type (x :: Symbol) /= (y :: Symbol) Source # |
Instance details Defined in Data.Singletons.TypeLits.Internal type (x :: Symbol) /= (y :: Symbol) = Not (x == y)
type Compare (a :: Symbol) (b :: Symbol) Source # |
Instance details Defined in Data.Singletons.TypeLits.Internal type Compare (a :: Symbol) (b :: Symbol) = CmpSymbol a b
type (arg1 :: Symbol) < (arg2 :: Symbol) Source # |
Instance details Defined in Data.Singletons.TypeLits.Internal type (arg1 :: Symbol) < (arg2 :: Symbol)
type (arg1 :: Symbol) <= (arg2 :: Symbol) Source # |
Instance details Defined in Data.Singletons.TypeLits.Internal type (arg1 :: Symbol) <= (arg2 :: Symbol)
type (arg1 :: Symbol) > (arg2 :: Symbol) Source # |
Instance details Defined in Data.Singletons.TypeLits.Internal type (arg1 :: Symbol) > (arg2 :: Symbol)
type (arg1 :: Symbol) >= (arg2 :: Symbol) Source # |
Instance details Defined in Data.Singletons.TypeLits.Internal type (arg1 :: Symbol) >= (arg2 :: Symbol)
type Max (arg1 :: Symbol) (arg2 :: Symbol) Source # |
Instance details Defined in Data.Singletons.TypeLits.Internal type Max (arg1 :: Symbol) (arg2 :: Symbol)
type Min (arg1 :: Symbol) (arg2 :: Symbol) Source # |
Instance details Defined in Data.Singletons.TypeLits.Internal type Min (arg1 :: Symbol) (arg2 :: Symbol)
type (a :: Symbol) <> (b :: Symbol) Source # |
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type (a :: Symbol) <> (b :: Symbol) = AppendSymbol a b
type ShowList (arg1 :: [Symbol]) arg2 Source # |
Instance details Defined in Data.Singletons.Prelude.Show type ShowList (arg1 :: [Symbol]) arg2
type Mappend (arg1 :: Symbol) (arg2 :: Symbol) Source # |
Instance details Defined in Data.Singletons.Prelude.Monoid type Mappend (arg1 :: Symbol) (arg2 :: Symbol)
type Apply KnownSymbolSym0 (n6989586621679482152 :: Symbol) Source # |
Instance details Defined in Data.Singletons.TypeLits type Apply KnownSymbolSym0 (n6989586621679482152 :: Symbol) = KnownSymbol n6989586621679482152
type Apply ShowSpaceSym0 (a6989586621680291114 :: Symbol) Source # |
Instance details Defined in Data.Singletons.Prelude.Show type Apply ShowSpaceSym0 (a6989586621680291114 :: Symbol) = ShowSpace a6989586621680291114
type Apply ShowCommaSpaceSym0 (a6989586621680291109 :: Symbol) Source # |
Instance details Defined in Data.Singletons.Prelude.Show type Apply ShowCommaSpaceSym0 (a6989586621680291109 :: Symbol) = ShowCommaSpace a6989586621680291109
type ShowsPrec a1 (a2 :: Symbol) a3 Source # |
Instance details Defined in Data.Singletons.Prelude.Show type ShowsPrec a1 (a2 :: Symbol) a3
type Apply (ShowCharSym1 a6989586621680291151 :: TyFun Symbol Symbol -> Type) (a6989586621680291152 :: Symbol) Source # |
Instance details Defined in Data.Singletons.Prelude.Show type Apply (ShowCharSym1 a6989586621680291151 :: TyFun Symbol Symbol -> Type) (a6989586621680291152 :: Symbol) = ShowChar a6989586621680291151 a6989586621680291152
type Apply (ShowStringSym1 a6989586621680291141 :: TyFun Symbol Symbol -> Type) (a6989586621680291142 :: Symbol) Source # |
Instance details Defined in Data.Singletons.Prelude.Show type Apply (ShowStringSym1 a6989586621680291141 :: TyFun Symbol Symbol -> Type) (a6989586621680291142 :: Symbol) = ShowString a6989586621680291141 a6989586621680291142
type Apply (FromStringSym0 :: TyFun Symbol k2 -> Type) (arg6989586621681259551 :: Symbol) Source # |
Instance details Defined in Data.Singletons.Prelude.IsString type Apply (FromStringSym0 :: TyFun Symbol k2 -> Type) (arg6989586621681259551 :: Symbol) = FromString arg6989586621681259551 :: k2
type Apply (Show_Sym0 :: TyFun a Symbol -> Type) (arg6989586621680291191 :: a) Source # |
Instance details Defined in Data.Singletons.Prelude.Show type Apply (Show_Sym0 :: TyFun a Symbol -> Type) (arg6989586621680291191 :: a) = Show_ arg6989586621680291191
type Apply (TypeErrorSym0 :: TyFun PErrorMessage k2 -> Type) (a6989586621681327364 :: PErrorMessage) Source # |
Instance details Defined in Data.Singletons.TypeError type Apply (TypeErrorSym0 :: TyFun PErrorMessage k2 -> Type) (a6989586621681327364 :: PErrorMessage) = TypeError a6989586621681327364 :: k2
type Apply (ShowListSym1 arg6989586621680291193 :: TyFun Symbol Symbol -> Type) (arg6989586621680291194 :: Symbol) Source # |
Instance details Defined in Data.Singletons.Prelude.Show type Apply (ShowListSym1 arg6989586621680291193 :: TyFun Symbol Symbol -> Type) (arg6989586621680291194 :: Symbol) = ShowList arg6989586621680291193 arg6989586621680291194
type Apply (ShowsSym1 a6989586621680291177 :: TyFun Symbol Symbol -> Type) (a6989586621680291178 :: Symbol) Source # |
Instance details Defined in Data.Singletons.Prelude.Show type Apply (ShowsSym1 a6989586621680291177 :: TyFun Symbol Symbol -> Type) (a6989586621680291178 :: Symbol) = Shows a6989586621680291177 a6989586621680291178
type Apply (ShowParenSym2 a6989586621680291124 a6989586621680291123 :: TyFun Symbol Symbol -> Type) (a6989586621680291125 :: Symbol) Source # |
Instance details Defined in Data.Singletons.Prelude.Show type Apply (ShowParenSym2 a6989586621680291124 a6989586621680291123 :: TyFun Symbol Symbol -> Type) (a6989586621680291125 :: Symbol) = ShowParen a6989586621680291124 a6989586621680291123 a6989586621680291125
type Apply (ShowsPrecSym2 arg6989586621680291186 arg6989586621680291185 :: TyFun Symbol Symbol -> Type) (arg6989586621680291187 :: Symbol) Source # |
Instance details Defined in Data.Singletons.Prelude.Show type Apply (ShowsPrecSym2 arg6989586621680291186 arg6989586621680291185 :: TyFun Symbol Symbol -> Type) (arg6989586621680291187 :: Symbol) = ShowsPrec arg6989586621680291186 arg6989586621680291185 arg6989586621680291187
type Apply (ShowListWithSym2 a6989586621680291158 a6989586621680291157 :: TyFun Symbol Symbol -> Type) (a6989586621680291159 :: Symbol) Source # |
Instance details Defined in Data.Singletons.Prelude.Show type Apply (ShowListWithSym2 a6989586621680291158 a6989586621680291157 :: TyFun Symbol Symbol -> Type) (a6989586621680291159 :: Symbol) = ShowListWith a6989586621680291158 a6989586621680291157 a6989586621680291159
type Apply ShowParenSym0 (a6989586621680291123 :: Bool) Source # |
Instance details Defined in Data.Singletons.Prelude.Show type Apply ShowParenSym0 (a6989586621680291123 :: Bool) = ShowParenSym1 a6989586621680291123
type Apply ShowCharSym0 (a6989586621680291151 :: Symbol) Source # |
Instance details Defined in Data.Singletons.Prelude.Show type Apply ShowCharSym0 (a6989586621680291151 :: Symbol) = ShowCharSym1 a6989586621680291151
type Apply ShowStringSym0 (a6989586621680291141 :: Symbol) Source # |
Instance details Defined in Data.Singletons.Prelude.Show type Apply ShowStringSym0 (a6989586621680291141 :: Symbol) = ShowStringSym1 a6989586621680291141
type Apply (ShowsPrecSym0 :: TyFun Nat (a6989586621680290747 ~> (Symbol ~> Symbol)) -> Type) (arg6989586621680291185 :: Nat) Source # |
Instance details Defined in Data.Singletons.Prelude.Show type Apply (ShowsPrecSym0 :: TyFun Nat (a6989586621680290747 ~> (Symbol ~> Symbol)) -> Type) (arg6989586621680291185 :: Nat) = ShowsPrecSym1 arg6989586621680291185 a6989586621680290747 :: TyFun a6989586621680290747 (Symbol ~> Symbol) -> Type
type Apply (ShowsSym0 :: TyFun a6989586621680290732 (Symbol ~> Symbol) -> Type) (a6989586621680291177 :: a6989586621680290732) Source # |
Instance details Defined in Data.Singletons.Prelude.Show type Apply (ShowsSym0 :: TyFun a6989586621680290732 (Symbol ~> Symbol) -> Type) (a6989586621680291177 :: a6989586621680290732) = ShowsSym1 a6989586621680291177
type Apply (ShowsPrecSym1 arg6989586621680291185 a6989586621680290747 :: TyFun a6989586621680290747 (Symbol ~> Symbol) -> Type) (arg6989586621680291186 :: a6989586621680290747) Source # |
Instance details Defined in Data.Singletons.Prelude.Show type Apply (ShowsPrecSym1 arg6989586621680291185 a6989586621680290747 :: TyFun a6989586621680290747 (Symbol ~> Symbol) -> Type) (arg6989586621680291186 :: a6989586621680290747) = ShowsPrecSym2 arg6989586621680291185 arg6989586621680291186
type Apply UnlinesSym0 (a6989586621679974943 :: [Symbol]) Source # |
Instance details Defined in Data.Singletons.Prelude.List.Internal type Apply UnlinesSym0 (a6989586621679974943 :: [Symbol]) = Unlines a6989586621679974943
type Apply UnwordsSym0 (a6989586621679974932 :: [Symbol]) Source # |
Instance details Defined in Data.Singletons.Prelude.List.Internal type Apply UnwordsSym0 (a6989586621679974932 :: [Symbol]) = Unwords a6989586621679974932
type Apply (ShowListSym0 :: TyFun [a6989586621680290747] (Symbol ~> Symbol) -> Type) (arg6989586621680291193 :: [a6989586621680290747]) Source # |
Instance details Defined in Data.Singletons.Prelude.Show type Apply (ShowListSym0 :: TyFun [a6989586621680290747] (Symbol ~> Symbol) -> Type) (arg6989586621680291193 :: [a6989586621680290747]) = ShowListSym1 arg6989586621680291193
type Apply (ShowListWithSym1 a6989586621680291157 :: TyFun [a6989586621680290731] (Symbol ~> Symbol) -> Type) (a6989586621680291158 :: [a6989586621680290731]) Source # |
Instance details Defined in Data.Singletons.Prelude.Show type Apply (ShowListWithSym1 a6989586621680291157 :: TyFun [a6989586621680290731] (Symbol ~> Symbol) -> Type) (a6989586621680291158 :: [a6989586621680290731]) = ShowListWithSym2 a6989586621680291157 a6989586621680291158
type Apply (ShowParenSym1 a6989586621680291123 :: TyFun (Symbol ~> Symbol) (Symbol ~> Symbol) -> Type) (a6989586621680291124 :: Symbol ~> Symbol) Source # |
Instance details Defined in Data.Singletons.Prelude.Show type Apply (ShowParenSym1 a6989586621680291123 :: TyFun (Symbol ~> Symbol) (Symbol ~> Symbol) -> Type) (a6989586621680291124 :: Symbol ~> Symbol) = ShowParenSym2 a6989586621680291123 a6989586621680291124
type Apply (ShowListWithSym0 :: TyFun (a6989586621680290731 ~> (Symbol ~> Symbol)) ([a6989586621680290731] ~> (Symbol ~> Symbol)) -> Type) (a6989586621680291157 :: a6989586621680290731 ~> (Symbol ~> Symbol)) Source # |
Instance details Defined in Data.Singletons.Prelude.Show type Apply (ShowListWithSym0 :: TyFun (a6989586621680290731 ~> (Symbol ~> Symbol)) ([a6989586621680290731] ~> (Symbol ~> Symbol)) -> Type) (a6989586621680291157 :: a6989586621680290731 ~> (Symbol ~> Symbol)) = ShowListWithSym1 a6989586621680291157

type family Sing :: k -> Type Source #

The singleton kind-indexed type family.

#### Instances

Instances details

type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = SBool
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = SOrdering
type Sing Source # |
Instance details Defined in Data.Singletons.TypeLits.Internal type Sing = SNat
type Sing Source # |
Instance details Defined in Data.Singletons.TypeLits.Internal type Sing = SSymbol
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = STuple0
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = SVoid
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type Sing = SAll
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type Sing = SAny
type Sing Source # |
Instance details Defined in Data.Singletons.TypeError type Sing = SErrorMessage
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = SList :: [a] -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = SMaybe :: Maybe a -> Type

type Sing Source #

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

Conceivably, one could generalize this instance to `Sing @k` 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 `TypeRep`s (for instance, `TypeRep`s are more difficult to pattern match on, and require extra runtime checks).

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

Instance details Defined in Data.Singletons.TypeRepTYPE type Sing = TypeRep :: TYPE rep -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = SNonEmpty :: NonEmpty a -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Ord type Sing = SDown :: Down a -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = SIdentity :: Identity a -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type Sing = SFirst :: First a -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type Sing = SLast :: Last a -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type Sing = SMax :: Max a -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type Sing = SMin :: Min a -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type Sing = SOption :: Option a -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type Sing = SWrappedMonoid :: WrappedMonoid m -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type Sing = SDual :: Dual a -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type Sing = SProduct :: Product a -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type Sing = SSum :: Sum a -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Monoid type Sing = SFirst :: First a -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Monoid type Sing = SLast :: Last a -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = SEither :: Either a b -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = STuple2 :: (a, b) -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Internal type Sing = SLambda :: (k1 ~> k2) -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Internal type Sing = SWrappedSing :: WrappedSing a -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Semigroup type Sing = SArg :: Arg a b -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Sigma type Sing = SSigma :: Sigma s t -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = STuple3 :: (a, b, c) -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Const type Sing = SConst :: Const a b -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = STuple4 :: (a, b, c, d) -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = STuple5 :: (a, b, c, d, e) -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = STuple6 :: (a, b, c, d, e, f) -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = STuple7 :: (a, b, c, d, e, f, g) -> Type

data SNat (n :: Nat) Source #

Constructors

KnownNat n => SNat |

#### Instances

Instances details

Show (SNat n) |
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> SNat n -> ShowS show :: SNat n -> String showList :: [SNat n] -> ShowS

data SSymbol (n :: Symbol) Source #

Constructors

KnownSymbol n => SSym |

#### Instances

Instances details

Show (SSymbol s) |
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> SSymbol s -> ShowS show :: SSymbol s -> String showList :: [SSymbol s] -> ShowS

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

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

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

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

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

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

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

The singleton for `error`

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

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

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

The singleton for `errorWithoutStackTrace`.

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

The promotion of `undefined`.

sUndefined :: HasCallStack => a Source #

The singleton for `undefined`.

class KnownNat (n :: Nat) #

Minimal complete definition

natSing

natVal :: forall (n :: Nat) proxy. KnownNat n => proxy n -> Natural #

class KnownSymbol (n :: Symbol) #

Minimal complete definition

symbolSing

symbolVal :: forall (n :: Symbol) proxy. KnownSymbol n => proxy n -> String #

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

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

The singleton analogue of `(^)` for `Nat`s.

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

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

The singleton analogue of `<=?`

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

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

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

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

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

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

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

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

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_6989586621679504196 a_6989586621679504198 = Apply (Apply DivSym0 a_6989586621679504196) a_6989586621679504198 |

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_6989586621679504186 a_6989586621679504188 = Apply (Apply ModSym0 a_6989586621679504186) a_6989586621679504188 |

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_6989586621679504206 a_6989586621679504208 = Apply (Apply DivModSym0 a_6989586621679504206) a_6989586621679504208 |

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

# Defunctionalization symbols

data ErrorSym0 :: forall k06989586621679481929 k6989586621679481930. (~>) k06989586621679481929 k6989586621679481930 Source #

#### Instances

Instances details

SingI (ErrorSym0 :: TyFun Symbol a -> Type) Source # |
Instance details Defined in Data.Singletons.TypeLits.Internal Methods sing :: Sing ErrorSym0 Source #
SuppressUnusedWarnings (ErrorSym0 :: TyFun k06989586621679481929 k6989586621679481930 -> Type) Source # |
Instance details Defined in Data.Singletons.TypeLits.Internal Methods suppressUnusedWarnings :: () Source #
type Apply (ErrorSym0 :: TyFun k0 k2 -> Type) (str6989586621679481931 :: k0) Source # |
Instance details Defined in Data.Singletons.TypeLits.Internal type Apply (ErrorSym0 :: TyFun k0 k2 -> Type) (str6989586621679481931 :: k0) = Error str6989586621679481931 :: k2

type ErrorSym1 (str6989586621679481931 :: k06989586621679481929) = Error str6989586621679481931 Source #

data ErrorWithoutStackTraceSym0 :: forall k06989586621679483019 k6989586621679483020. (~>) k06989586621679483019 k6989586621679483020 Source #

#### Instances

Instances details

SingI (ErrorWithoutStackTraceSym0 :: TyFun Symbol a -> Type) Source # |
Instance details Defined in Data.Singletons.TypeLits.Internal Methods sing :: Sing ErrorWithoutStackTraceSym0 Source #
SuppressUnusedWarnings (ErrorWithoutStackTraceSym0 :: TyFun k06989586621679483019 k6989586621679483020 -> Type) Source # |
Instance details Defined in Data.Singletons.TypeLits.Internal Methods suppressUnusedWarnings :: () Source #
type Apply (ErrorWithoutStackTraceSym0 :: TyFun k0 k2 -> Type) (str6989586621679483021 :: k0) Source # |
Instance details Defined in Data.Singletons.TypeLits.Internal type Apply (ErrorWithoutStackTraceSym0 :: TyFun k0 k2 -> Type) (str6989586621679483021 :: k0) = ErrorWithoutStackTrace str6989586621679483021 :: k2

type ErrorWithoutStackTraceSym1 (str6989586621679483021 :: k06989586621679483019) = ErrorWithoutStackTrace str6989586621679483021 Source #

type UndefinedSym0 = Undefined Source #

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

#### Instances

Instances details

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

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

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

#### Instances

Instances details

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

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

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

#### Instances

Instances details

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

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

#### Instances

Instances details

SingI x => SingI ((^@#@$$) x :: TyFun Nat Nat -> Type) Source # |
Instance details Defined in Data.Singletons.TypeLits.Internal Methods sing :: Sing ((^@#@$$) x) Source #
SuppressUnusedWarnings ((^@#@$$) a3530822107858468865 :: TyFun Nat Nat -> Type) Source # |
Instance details Defined in Data.Singletons.TypeLits.Internal Methods suppressUnusedWarnings :: () Source #
type Apply ((^@#@$$) a3530822107858468865 :: TyFun Nat Nat -> Type) (b3530822107858468866 :: Nat) Source # |
Instance details Defined in Data.Singletons.TypeLits.Internal type Apply ((^@#@$$) a3530822107858468865 :: TyFun Nat Nat -> Type) (b3530822107858468866 :: Nat) = a3530822107858468865 ^ b3530822107858468866

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

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

#### Instances

Instances details

SingI (<=?@#@$) Source # |
Instance details Defined in Data.Singletons.TypeLits.Internal Methods sing :: Sing (<=?@#@$) Source #
SuppressUnusedWarnings (<=?@#@$) Source # |
Instance details Defined in Data.Singletons.TypeLits.Internal Methods suppressUnusedWarnings :: () Source #
type Apply (<=?@#@$) (a3530822107858468865 :: Nat) Source # |
Instance details Defined in Data.Singletons.TypeLits.Internal type Apply (<=?@#@$) (a3530822107858468865 :: Nat) = (<=?@#@$$) a3530822107858468865

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

#### Instances

Instances details

SingI x => SingI ((<=?@#@$$) x :: TyFun Nat Bool -> Type) Source # |
Instance details Defined in Data.Singletons.TypeLits.Internal Methods sing :: Sing ((<=?@#@$$) x) Source #
SuppressUnusedWarnings ((<=?@#@$$) a3530822107858468865 :: TyFun Nat Bool -> Type) Source # |
Instance details Defined in Data.Singletons.TypeLits.Internal Methods suppressUnusedWarnings :: () Source #
type Apply ((<=?@#@$$) a3530822107858468865 :: TyFun Nat Bool -> Type) (b3530822107858468866 :: Nat) Source # |
Instance details Defined in Data.Singletons.TypeLits.Internal type Apply ((<=?@#@$$) a3530822107858468865 :: TyFun Nat Bool -> Type) (b3530822107858468866 :: Nat) = a3530822107858468865 <=? b3530822107858468866

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

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

#### Instances

Instances details

SingI Log2Sym0 Source # |
Instance details Defined in Data.Singletons.TypeLits Methods sing :: Sing Log2Sym0 Source #
SuppressUnusedWarnings Log2Sym0 Source # |
Instance details Defined in Data.Singletons.TypeLits Methods suppressUnusedWarnings :: () Source #
type Apply Log2Sym0 (a3530822107858468865 :: Nat) Source # |
Instance details Defined in Data.Singletons.TypeLits type Apply Log2Sym0 (a3530822107858468865 :: Nat) = Log2 a3530822107858468865

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

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

#### Instances

Instances details

SingI DivSym0 Source # |
Instance details Defined in Data.Singletons.TypeLits Methods sing :: Sing DivSym0 Source #
SuppressUnusedWarnings DivSym0 Source # |
Instance details Defined in Data.Singletons.TypeLits Methods suppressUnusedWarnings :: () Source #
type Apply DivSym0 (a3530822107858468865 :: Nat) Source # |
Instance details Defined in Data.Singletons.TypeLits type Apply DivSym0 (a3530822107858468865 :: Nat) = DivSym1 a3530822107858468865

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

#### Instances

Instances details

SingI x => SingI (DivSym1 x :: TyFun Nat Nat -> Type) Source # |
Instance details Defined in Data.Singletons.TypeLits Methods sing :: Sing (DivSym1 x) Source #
SuppressUnusedWarnings (DivSym1 a3530822107858468865 :: TyFun Nat Nat -> Type) Source # |
Instance details Defined in Data.Singletons.TypeLits Methods suppressUnusedWarnings :: () Source #
type Apply (DivSym1 a3530822107858468865 :: TyFun Nat Nat -> Type) (b3530822107858468866 :: Nat) Source # |
Instance details Defined in Data.Singletons.TypeLits type Apply (DivSym1 a3530822107858468865 :: TyFun Nat Nat -> Type) (b3530822107858468866 :: Nat) = Div a3530822107858468865 b3530822107858468866

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

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

#### Instances

Instances details

SingI ModSym0 Source # |
Instance details Defined in Data.Singletons.TypeLits Methods sing :: Sing ModSym0 Source #
SuppressUnusedWarnings ModSym0 Source # |
Instance details Defined in Data.Singletons.TypeLits Methods suppressUnusedWarnings :: () Source #
type Apply ModSym0 (a3530822107858468865 :: Nat) Source # |
Instance details Defined in Data.Singletons.TypeLits type Apply ModSym0 (a3530822107858468865 :: Nat) = ModSym1 a3530822107858468865

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

#### Instances

Instances details

SingI x => SingI (ModSym1 x :: TyFun Nat Nat -> Type) Source # |
Instance details Defined in Data.Singletons.TypeLits Methods sing :: Sing (ModSym1 x) Source #
SuppressUnusedWarnings (ModSym1 a3530822107858468865 :: TyFun Nat Nat -> Type) Source # |
Instance details Defined in Data.Singletons.TypeLits Methods suppressUnusedWarnings :: () Source #
type Apply (ModSym1 a3530822107858468865 :: TyFun Nat Nat -> Type) (b3530822107858468866 :: Nat) Source # |
Instance details Defined in Data.Singletons.TypeLits type Apply (ModSym1 a3530822107858468865 :: TyFun Nat Nat -> Type) (b3530822107858468866 :: Nat) = Mod a3530822107858468865 b3530822107858468866

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

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

#### Instances

Instances details

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

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

#### Instances

Instances details

SuppressUnusedWarnings (DivModSym1 a6989586621679504216 :: TyFun Nat (Nat, Nat) -> Type) Source # |
Instance details Defined in Data.Singletons.TypeLits Methods suppressUnusedWarnings :: () Source #
type Apply (DivModSym1 a6989586621679504216 :: TyFun Nat (Nat, Nat) -> Type) (a6989586621679504217 :: Nat) Source # |
Instance details Defined in Data.Singletons.TypeLits type Apply (DivModSym1 a6989586621679504216 :: TyFun Nat (Nat, Nat) -> Type) (a6989586621679504217 :: Nat) = DivMod a6989586621679504216 a6989586621679504217

type DivModSym2 (a6989586621679504216 :: Nat) (a6989586621679504217 :: Nat) = DivMod a6989586621679504216 a6989586621679504217 Source #

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

#### Instances

Instances details

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

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

#### Instances

Instances details

SuppressUnusedWarnings (QuotSym1 a6989586621679504200 :: TyFun Nat Nat -> Type) Source # |
Instance details Defined in Data.Singletons.TypeLits Methods suppressUnusedWarnings :: () Source #
type Apply (QuotSym1 a6989586621679504200 :: TyFun Nat Nat -> Type) (a6989586621679504201 :: Nat) Source # |
Instance details Defined in Data.Singletons.TypeLits type Apply (QuotSym1 a6989586621679504200 :: TyFun Nat Nat -> Type) (a6989586621679504201 :: Nat) = Quot a6989586621679504200 a6989586621679504201

type QuotSym2 (a6989586621679504200 :: Nat) (a6989586621679504201 :: Nat) = Quot a6989586621679504200 a6989586621679504201 Source #

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

#### Instances

Instances details

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

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

#### Instances

Instances details

SuppressUnusedWarnings (RemSym1 a6989586621679504190 :: TyFun Nat Nat -> Type) Source # |
Instance details Defined in Data.Singletons.TypeLits Methods suppressUnusedWarnings :: () Source #
type Apply (RemSym1 a6989586621679504190 :: TyFun Nat Nat -> Type) (a6989586621679504191 :: Nat) Source # |
Instance details Defined in Data.Singletons.TypeLits type Apply (RemSym1 a6989586621679504190 :: TyFun Nat Nat -> Type) (a6989586621679504191 :: Nat) = Rem a6989586621679504190 a6989586621679504191

type RemSym2 (a6989586621679504190 :: Nat) (a6989586621679504191 :: Nat) = Rem a6989586621679504190 a6989586621679504191 Source #

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

#### Instances

Instances details

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

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

#### Instances

Instances details

SuppressUnusedWarnings (QuotRemSym1 a6989586621679504210 :: TyFun Nat (Nat, Nat) -> Type) Source # |
Instance details Defined in Data.Singletons.TypeLits Methods suppressUnusedWarnings :: () Source #
type Apply (QuotRemSym1 a6989586621679504210 :: TyFun Nat (Nat, Nat) -> Type) (a6989586621679504211 :: Nat) Source # |
Instance details Defined in Data.Singletons.TypeLits type Apply (QuotRemSym1 a6989586621679504210 :: TyFun Nat (Nat, Nat) -> Type) (a6989586621679504211 :: Nat) = QuotRem a6989586621679504210 a6989586621679504211

type QuotRemSym2 (a6989586621679504210 :: Nat) (a6989586621679504211 :: Nat) = QuotRem a6989586621679504210 a6989586621679504211 Source #

# Orphan instances

Enum Nat Source # |
Instance details 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 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
Show Nat Source # |
Instance details Methods showsPrec :: Int -> Nat -> ShowS show :: Nat -> String showList :: [Nat] -> ShowS
Show Symbol Source # |
Instance details Methods showsPrec :: Int -> Symbol -> ShowS show :: Symbol -> String showList :: [Symbol] -> ShowS
IsString Symbol Source # |
Instance details Methods fromString :: String -> Symbol
Semigroup Symbol Source # |
Instance details Methods (<>) :: Symbol -> Symbol -> Symbol sconcat :: NonEmpty Symbol -> Symbol stimes :: Integral b => b -> Symbol -> Symbol
Monoid Symbol Source # |
Instance details Methods mempty :: Symbol mappend :: Symbol -> Symbol -> Symbol mconcat :: [Symbol] -> Symbol