Copyright	(C) 2014 Richard Eisenberg
License	BSD-style (see LICENSE)
Maintainer	Ryan Scott
Stability	experimental
Portability	non-portable
Safe Haskell	None
Language	Haskell2010

GHC.TypeLits.Singletons

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 :: (~>) k0 k
type family ErrorSym1 (a6989586621679518606 :: k0) :: k where ...
data ErrorWithoutStackTraceSym0 :: (~>) k0 k
type family ErrorWithoutStackTraceSym1 (a6989586621679518903 :: k0) :: k where ...
type family UndefinedSym0 :: k where ...
data KnownNatSym0 :: (~>) Nat Constraint
type family KnownNatSym1 (a6989586621679528269 :: Nat) :: Constraint where ...
data KnownSymbolSym0 :: (~>) Symbol Constraint
type family KnownSymbolSym1 (a6989586621679528271 :: Symbol) :: Constraint where ...
data (^@#@$) :: (~>) Nat ((~>) Nat Nat)
data (^@#@$$) (a6989586621679519847 :: Nat) :: (~>) Nat Nat
type family (a6989586621679519847 :: Nat) ^@#@$$$ (a6989586621679519848 :: Nat) :: Nat where ...
data (<=?@#@$) :: (~>) Nat ((~>) Nat Bool)
data (<=?@#@$$) (a6989586621679520207 :: Nat) :: (~>) Nat Bool
type family (a6989586621679520207 :: Nat) <=?@#@$$$ (a6989586621679520208 :: Nat) :: Bool where ...
data Log2Sym0 :: (~>) Nat Nat
type family Log2Sym1 (a6989586621679528808 :: Nat) :: Nat where ...
data DivSym0 :: (~>) Nat ((~>) Nat Nat)
data DivSym1 (a6989586621679529054 :: Nat) :: (~>) Nat Nat
type family DivSym2 (a6989586621679529054 :: Nat) (a6989586621679529055 :: Nat) :: Nat where ...
data ModSym0 :: (~>) Nat ((~>) Nat Nat)
data ModSym1 (a6989586621679529457 :: Nat) :: (~>) Nat Nat
type family ModSym2 (a6989586621679529457 :: Nat) (a6989586621679529458 :: Nat) :: Nat where ...
data DivModSym0 :: (~>) Nat ((~>) Nat (Nat, Nat))
data DivModSym1 (a6989586621679530018 :: Nat) :: (~>) Nat (Nat, Nat)
type family DivModSym2 (a6989586621679530018 :: Nat) (a6989586621679530019 :: Nat) :: (Nat, Nat) where ...
data QuotSym0 :: (~>) Nat ((~>) Nat Nat)
data QuotSym1 (a6989586621679530000 :: Nat) :: (~>) Nat Nat
type family QuotSym2 (a6989586621679530000 :: Nat) (a6989586621679530001 :: Nat) :: Nat where ...
data RemSym0 :: (~>) Nat ((~>) Nat Nat)
data RemSym1 (a6989586621679529989 :: Nat) :: (~>) Nat Nat
type family RemSym2 (a6989586621679529989 :: Nat) (a6989586621679529990 :: Nat) :: Nat where ...
data QuotRemSym0 :: (~>) Nat ((~>) Nat (Nat, Nat))
data QuotRemSym1 (a6989586621679530011 :: Nat) :: (~>) Nat (Nat, Nat)
type family QuotRemSym2 (a6989586621679530011 :: Nat) (a6989586621679530012 :: Nat) :: (Nat, Nat) where ...

Documentation

data Nat #

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

Instances

Instances details

Enum Nat Source #
Instance details Defined in GHC.TypeLits.Singletons 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 Defined in GHC.TypeLits.Singletons Methods (==) :: Nat -> Nat -> Bool # (/=) :: Nat -> Nat -> 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 Defined in GHC.TypeLits.Singletons 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 Defined in GHC.TypeLits.Singletons 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 Source #
Instance details Defined in GHC.TypeLits.Singletons Methods showsPrec :: Int -> Nat -> ShowS # show :: Nat -> String # showList :: [Nat] -> ShowS #
SDecide Nat Source #
Instance details Defined in GHC.TypeLits.Singletons.Internal Methods (%~) :: forall (a :: Nat) (b :: Nat). Sing a -> Sing b -> Decision (a :~: b) #
SingKind Nat Source #
Instance details Defined in GHC.TypeLits.Singletons.Internal Associated Types type Demote Nat = (r :: Type) # Methods fromSing :: forall (a :: Nat). Sing a -> Demote Nat # toSing :: Demote Nat -> SomeSing Nat #
SEq Nat Source #
Instance details Defined in GHC.TypeLits.Singletons.Internal 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 #
PEq Nat Source #
Instance details Defined in GHC.TypeLits.Singletons.Internal Associated Types type arg == arg :: Bool Source # type arg /= arg :: Bool Source #
SOrd Nat Source #
Instance details Defined in GHC.TypeLits.Singletons.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 GHC.TypeLits.Singletons.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 GHC.Num.Singletons 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 GHC.Num.Singletons 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.Base.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.Base.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 Text.Show.Singletons 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 Text.Show.Singletons 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 GHC.TypeLits.Singletons.Internal Methods sing :: Sing n #
SingI Log2Sym0 Source #
Instance details Defined in GHC.TypeLits.Singletons Methods sing :: Sing Log2Sym0 #
SingI (<=?@#@$) Source #
Instance details Defined in GHC.TypeLits.Singletons.Internal Methods sing :: Sing (<=?@#@$) #
SingI (^@#@$) Source #
Instance details Defined in GHC.TypeLits.Singletons.Internal Methods sing :: Sing (^@#@$) #
SingI DivSym0 Source #
Instance details Defined in GHC.TypeLits.Singletons Methods sing :: Sing DivSym0 #
SingI ModSym0 Source #
Instance details Defined in GHC.TypeLits.Singletons Methods sing :: Sing ModSym0 #
SuppressUnusedWarnings KnownNatSym0 Source #
Instance details Defined in GHC.TypeLits.Singletons Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings Log2Sym0 Source #
Instance details Defined in GHC.TypeLits.Singletons Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (<=?@#@$) Source #
Instance details Defined in GHC.TypeLits.Singletons.Internal Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (^@#@$) Source #
Instance details Defined in GHC.TypeLits.Singletons.Internal Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings DivSym0 Source #
Instance details Defined in GHC.TypeLits.Singletons Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings ModSym0 Source #
Instance details Defined in GHC.TypeLits.Singletons Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings QuotSym0 Source #
Instance details Defined in GHC.TypeLits.Singletons Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings RemSym0 Source #
Instance details Defined in GHC.TypeLits.Singletons Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings DivModSym0 Source #
Instance details Defined in GHC.TypeLits.Singletons Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings QuotRemSym0 Source #
Instance details Defined in GHC.TypeLits.Singletons Methods suppressUnusedWarnings :: () #
SingI x => SingI ((<=?@#@$$) x :: TyFun Nat Bool -> Type) Source #
Instance details Defined in GHC.TypeLits.Singletons.Internal Methods sing :: Sing ((<=?@#@$$) x) #
SingI x => SingI ((^@#@$$) x :: TyFun Nat Nat -> Type) Source #
Instance details Defined in GHC.TypeLits.Singletons.Internal Methods sing :: Sing ((^@#@$$) x) #
SingI x => SingI (DivSym1 x :: TyFun Nat Nat -> Type) Source #
Instance details Defined in GHC.TypeLits.Singletons Methods sing :: Sing (DivSym1 x) #
SingI x => SingI (ModSym1 x :: TyFun Nat Nat -> Type) Source #
Instance details Defined in GHC.TypeLits.Singletons Methods sing :: Sing (ModSym1 x) #
SingI ((!!@#@$) :: TyFun [a] (Nat ~> a) -> Type) Source #
Instance details Defined in Data.List.Singletons.Internal Methods sing :: Sing (!!@#@$) #
SNum a => SingI (FromIntegerSym0 :: TyFun Nat a -> Type) Source #
Instance details Defined in GHC.Num.Singletons Methods sing :: Sing FromIntegerSym0 #
SEnum a => SingI (ToEnumSym0 :: TyFun Nat a -> Type) Source #
Instance details Defined in Data.Singletons.Base.Enum Methods sing :: Sing ToEnumSym0 #
SingI (SplitAtSym0 :: TyFun Nat ([a] ~> ([a], [a])) -> Type) Source #
Instance details Defined in Data.List.Singletons.Internal Methods sing :: Sing SplitAtSym0 #
SingI (DropSym0 :: TyFun Nat ([a] ~> [a]) -> Type) Source #
Instance details Defined in Data.List.Singletons.Internal Methods sing :: Sing DropSym0 #
SingI (TakeSym0 :: TyFun Nat ([a] ~> [a]) -> Type) Source #
Instance details Defined in Data.List.Singletons.Internal Methods sing :: Sing TakeSym0 #
SingI (ReplicateSym0 :: TyFun Nat (a ~> [a]) -> Type) Source #
Instance details Defined in Data.List.Singletons.Internal Methods sing :: Sing ReplicateSym0 #
SShow a => SingI (ShowsPrecSym0 :: TyFun Nat (a ~> (Symbol ~> Symbol)) -> Type) Source #
Instance details Defined in Text.Show.Singletons Methods sing :: Sing ShowsPrecSym0 #
SingI (SplitAtSym0 :: TyFun Nat (NonEmpty a ~> ([a], [a])) -> Type) Source #
Instance details Defined in Data.List.NonEmpty.Singletons Methods sing :: Sing SplitAtSym0 #
SingI (DropSym0 :: TyFun Nat (NonEmpty a ~> [a]) -> Type) Source #
Instance details Defined in Data.List.NonEmpty.Singletons Methods sing :: Sing DropSym0 #
SingI (TakeSym0 :: TyFun Nat (NonEmpty a ~> [a]) -> Type) Source #
Instance details Defined in Data.List.NonEmpty.Singletons Methods sing :: Sing TakeSym0 #
SEnum a => SingI (FromEnumSym0 :: TyFun a Nat -> Type) Source #
Instance details Defined in Data.Singletons.Base.Enum Methods sing :: Sing FromEnumSym0 #
SEq a => SingI (ElemIndicesSym0 :: TyFun a ([a] ~> [Nat]) -> Type) Source #
Instance details Defined in Data.List.Singletons.Internal Methods sing :: Sing ElemIndicesSym0 #
SEq a => SingI (ElemIndexSym0 :: TyFun a ([a] ~> Maybe Nat) -> Type) Source #
Instance details Defined in Data.List.Singletons.Internal Methods sing :: Sing ElemIndexSym0 #
SingI ((!!@#@$) :: TyFun (NonEmpty a) (Nat ~> a) -> Type) Source #
Instance details Defined in Data.List.NonEmpty.Singletons Methods sing :: Sing (!!@#@$) #
SingI (LengthSym0 :: TyFun (NonEmpty a) Nat -> Type) Source #
Instance details Defined in Data.List.NonEmpty.Singletons Methods sing :: Sing LengthSym0 #
SingI (FindIndicesSym0 :: TyFun (a ~> Bool) ([a] ~> [Nat]) -> Type) Source #
Instance details Defined in Data.List.Singletons.Internal Methods sing :: Sing FindIndicesSym0 #
SingI (FindIndexSym0 :: TyFun (a ~> Bool) ([a] ~> Maybe Nat) -> Type) Source #
Instance details Defined in Data.List.Singletons.Internal Methods sing :: Sing FindIndexSym0 #
SuppressUnusedWarnings ((!!@#@$) :: TyFun [a] (Nat ~> a) -> Type) Source #
Instance details Defined in Data.List.Singletons.Internal Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings ((<=?@#@$$) a6989586621679520207 :: TyFun Nat Bool -> Type) Source #
Instance details Defined in GHC.TypeLits.Singletons.Internal Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings ((^@#@$$) a6989586621679519847 :: TyFun Nat Nat -> Type) Source #
Instance details Defined in GHC.TypeLits.Singletons.Internal Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (DivSym1 a6989586621679529054 :: TyFun Nat Nat -> Type) Source #
Instance details Defined in GHC.TypeLits.Singletons Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (ModSym1 a6989586621679529457 :: TyFun Nat Nat -> Type) Source #
Instance details Defined in GHC.TypeLits.Singletons Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (QuotSym1 a6989586621679530000 :: TyFun Nat Nat -> Type) Source #
Instance details Defined in GHC.TypeLits.Singletons Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (RemSym1 a6989586621679529989 :: TyFun Nat Nat -> Type) Source #
Instance details Defined in GHC.TypeLits.Singletons Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (DivModSym1 a6989586621679530018 :: TyFun Nat (Nat, Nat) -> Type) Source #
Instance details Defined in GHC.TypeLits.Singletons Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (QuotRemSym1 a6989586621679530011 :: TyFun Nat (Nat, Nat) -> Type) Source #
Instance details Defined in GHC.TypeLits.Singletons Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (FromIntegerSym0 :: TyFun Nat a -> Type) Source #
Instance details Defined in GHC.Num.Singletons Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (ToEnumSym0 :: TyFun Nat a -> Type) Source #
Instance details Defined in Data.Singletons.Base.Enum Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (DropSym0 :: TyFun Nat ([a] ~> [a]) -> Type) Source #
Instance details Defined in Data.List.Singletons.Internal Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (TakeSym0 :: TyFun Nat ([a] ~> [a]) -> Type) Source #
Instance details Defined in Data.List.Singletons.Internal Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (SplitAtSym0 :: TyFun Nat ([a] ~> ([a], [a])) -> Type) Source #
Instance details Defined in Data.List.Singletons.Internal Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (ReplicateSym0 :: TyFun Nat (a ~> [a]) -> Type) Source #
Instance details Defined in Data.List.Singletons.Internal Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (ShowsPrecSym0 :: TyFun Nat (a ~> (Symbol ~> Symbol)) -> Type) Source #
Instance details Defined in Text.Show.Singletons Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (TakeSym0 :: TyFun Nat (NonEmpty a ~> [a]) -> Type) Source #
Instance details Defined in Data.List.NonEmpty.Singletons Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (DropSym0 :: TyFun Nat (NonEmpty a ~> [a]) -> Type) Source #
Instance details Defined in Data.List.NonEmpty.Singletons Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (SplitAtSym0 :: TyFun Nat (NonEmpty a ~> ([a], [a])) -> Type) Source #
Instance details Defined in Data.List.NonEmpty.Singletons Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (FromEnumSym0 :: TyFun a Nat -> Type) Source #
Instance details Defined in Data.Singletons.Base.Enum Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (ElemIndicesSym0 :: TyFun a ([a] ~> [Nat]) -> Type) Source #
Instance details Defined in Data.List.Singletons.Internal Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (ElemIndexSym0 :: TyFun a ([a] ~> Maybe Nat) -> Type) Source #
Instance details Defined in Data.List.Singletons.Internal Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings ((!!@#@$) :: TyFun (NonEmpty a) (Nat ~> a) -> Type) Source #
Instance details Defined in Data.List.NonEmpty.Singletons Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (LengthSym0 :: TyFun (NonEmpty a) Nat -> Type) Source #
Instance details Defined in Data.List.NonEmpty.Singletons Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (FindIndicesSym0 :: TyFun (a ~> Bool) ([a] ~> [Nat]) -> Type) Source #
Instance details Defined in Data.List.Singletons.Internal Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (FindIndexSym0 :: TyFun (a ~> Bool) ([a] ~> Maybe Nat) -> Type) Source #
Instance details Defined in Data.List.Singletons.Internal Methods suppressUnusedWarnings :: () #
SingI d => SingI (FindIndicesSym1 d :: TyFun [a] [Nat] -> Type) Source #
Instance details Defined in Data.List.Singletons.Internal Methods sing :: Sing (FindIndicesSym1 d) #
SingI d => SingI (FindIndexSym1 d :: TyFun [a] (Maybe Nat) -> Type) Source #
Instance details Defined in Data.List.Singletons.Internal Methods sing :: Sing (FindIndexSym1 d) #
(SEq a, SingI d) => SingI (ElemIndicesSym1 d :: TyFun [a] [Nat] -> Type) Source #
Instance details Defined in Data.List.Singletons.Internal Methods sing :: Sing (ElemIndicesSym1 d) #
(SEq a, SingI d) => SingI (ElemIndexSym1 d :: TyFun [a] (Maybe Nat) -> Type) Source #
Instance details Defined in Data.List.Singletons.Internal Methods sing :: Sing (ElemIndexSym1 d) #
SingI d => SingI ((!!@#@$$) d :: TyFun Nat a -> Type) Source #
Instance details Defined in Data.List.Singletons.Internal Methods sing :: Sing ((!!@#@$$) d) #
SingI d => SingI ((!!@#@$$) d :: TyFun Nat a -> Type) Source #
Instance details Defined in Data.List.NonEmpty.Singletons Methods sing :: Sing ((!!@#@$$) d) #
SApplicative m => SingI (ReplicateM_Sym0 :: TyFun Nat (m a ~> m ()) -> Type) Source #
Instance details Defined in Control.Monad.Singletons Methods sing :: Sing ReplicateM_Sym0 #
SApplicative m => SingI (ReplicateMSym0 :: TyFun Nat (m a ~> m [a]) -> Type) Source #
Instance details Defined in Control.Monad.Singletons Methods sing :: Sing ReplicateMSym0 #
SuppressUnusedWarnings (FindIndicesSym1 a6989586621679814409 :: TyFun [a] [Nat] -> Type) Source #
Instance details Defined in Data.List.Singletons.Internal Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (ElemIndicesSym1 a6989586621679814441 :: TyFun [a] [Nat] -> Type) Source #
Instance details Defined in Data.List.Singletons.Internal Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (FindIndexSym1 a6989586621679814432 :: TyFun [a] (Maybe Nat) -> Type) Source #
Instance details Defined in Data.List.Singletons.Internal Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (ElemIndexSym1 a6989586621679814450 :: TyFun [a] (Maybe Nat) -> Type) Source #
Instance details Defined in Data.List.Singletons.Internal Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings ((!!@#@$$) a6989586621679814074 :: TyFun Nat a -> Type) Source #
Instance details Defined in Data.List.Singletons.Internal Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings ((!!@#@$$) a6989586621681120418 :: TyFun Nat a -> Type) Source #
Instance details Defined in Data.List.NonEmpty.Singletons Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (ReplicateM_Sym0 :: TyFun Nat (m a ~> m ()) -> Type) Source #
Instance details Defined in Control.Monad.Singletons Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (ReplicateMSym0 :: TyFun Nat (m a ~> m [a]) -> Type) Source #
Instance details Defined in Control.Monad.Singletons Methods suppressUnusedWarnings :: () #
SFoldable t => SingI (LengthSym0 :: TyFun (t a) Nat -> Type) Source #
Instance details Defined in Data.Foldable.Singletons Methods sing :: Sing LengthSym0 #
SuppressUnusedWarnings (LengthSym0 :: TyFun (t a) Nat -> Type) Source #
Instance details Defined in Data.Foldable.Singletons Methods suppressUnusedWarnings :: () #
type Sing Source #
Instance details Defined in GHC.TypeLits.Singletons.Internal type Sing = SNat
type Demote Nat Source #
Instance details Defined in GHC.TypeLits.Singletons.Internal type Demote Nat = Natural
type Negate (a :: Nat) Source #
Instance details Defined in GHC.Num.Singletons type Negate (a :: Nat) = Error "Cannot negate a natural number" :: Nat
type Abs (a :: Nat) Source #
Instance details Defined in GHC.Num.Singletons type Abs (a :: Nat) = a
type Signum (a :: Nat) Source #
Instance details Defined in GHC.Num.Singletons type Signum (a :: Nat)
type FromInteger a Source #
Instance details Defined in GHC.Num.Singletons type FromInteger a = a
type Succ (a :: Nat) Source #
Instance details Defined in Data.Singletons.Base.Enum type Succ (a :: Nat)
type Pred (a :: Nat) Source #
Instance details Defined in Data.Singletons.Base.Enum type Pred (a :: Nat)
type ToEnum a Source #
Instance details Defined in Data.Singletons.Base.Enum type ToEnum a
type FromEnum (a :: Nat) Source #
Instance details Defined in Data.Singletons.Base.Enum type FromEnum (a :: Nat)
type Show_ (arg :: Nat) Source #
Instance details Defined in Text.Show.Singletons type Show_ (arg :: Nat)
type (x :: Nat) == (y :: Nat) Source #
Instance details Defined in GHC.TypeLits.Singletons.Internal type (x :: Nat) == (y :: Nat) = DefaultEq x y
type (arg1 :: Nat) /= (arg2 :: Nat) Source #
Instance details Defined in GHC.TypeLits.Singletons.Internal type (arg1 :: Nat) /= (arg2 :: Nat)
type Compare (a :: Nat) (b :: Nat) Source #
Instance details Defined in GHC.TypeLits.Singletons.Internal type Compare (a :: Nat) (b :: Nat) = CmpNat a b
type (arg1 :: Nat) < (arg2 :: Nat) Source #
Instance details Defined in GHC.TypeLits.Singletons.Internal type (arg1 :: Nat) < (arg2 :: Nat)
type (arg1 :: Nat) <= (arg2 :: Nat) Source #
Instance details Defined in GHC.TypeLits.Singletons.Internal type (arg1 :: Nat) <= (arg2 :: Nat)
type (arg1 :: Nat) > (arg2 :: Nat) Source #
Instance details Defined in GHC.TypeLits.Singletons.Internal type (arg1 :: Nat) > (arg2 :: Nat)
type (arg1 :: Nat) >= (arg2 :: Nat) Source #
Instance details Defined in GHC.TypeLits.Singletons.Internal type (arg1 :: Nat) >= (arg2 :: Nat)
type Max (arg1 :: Nat) (arg2 :: Nat) Source #
Instance details Defined in GHC.TypeLits.Singletons.Internal type Max (arg1 :: Nat) (arg2 :: Nat)
type Min (arg1 :: Nat) (arg2 :: Nat) Source #
Instance details Defined in GHC.TypeLits.Singletons.Internal type Min (arg1 :: Nat) (arg2 :: Nat)
type (a :: Nat) + (b :: Nat) Source #
Instance details Defined in GHC.Num.Singletons type (a :: Nat) + (b :: Nat) = a + b
type (a :: Nat) - (b :: Nat) Source #
Instance details Defined in GHC.Num.Singletons type (a :: Nat) - (b :: Nat) = a - b
type (a :: Nat) * (b :: Nat) Source #
Instance details Defined in GHC.Num.Singletons type (a :: Nat) * (b :: Nat) = a * b
type EnumFromTo (a1 :: Nat) (a2 :: Nat) Source #
Instance details Defined in Data.Singletons.Base.Enum type EnumFromTo (a1 :: Nat) (a2 :: Nat)
type ShowList (arg1 :: [Nat]) arg2 Source #
Instance details Defined in Text.Show.Singletons type ShowList (arg1 :: [Nat]) arg2
type Apply KnownNatSym0 (a6989586621679528269 :: Nat) Source #
Instance details Defined in GHC.TypeLits.Singletons type Apply KnownNatSym0 (a6989586621679528269 :: Nat) = KnownNat a6989586621679528269
type Apply Log2Sym0 (a6989586621679528808 :: Nat) Source #
Instance details Defined in GHC.TypeLits.Singletons type Apply Log2Sym0 (a6989586621679528808 :: Nat) = Log2 a6989586621679528808
type EnumFromThenTo (a1 :: Nat) (a2 :: Nat) (a3 :: Nat) Source #
Instance details Defined in Data.Singletons.Base.Enum type EnumFromThenTo (a1 :: Nat) (a2 :: Nat) (a3 :: Nat)
type ShowsPrec _1 (n :: Nat) x Source #
Instance details Defined in Text.Show.Singletons type ShowsPrec _1 (n :: Nat) x
type Apply ((<=?@#@$$) a6989586621679520207 :: TyFun Nat Bool -> Type) (a6989586621679520208 :: Nat) Source #
Instance details Defined in GHC.TypeLits.Singletons.Internal type Apply ((<=?@#@$$) a6989586621679520207 :: TyFun Nat Bool -> Type) (a6989586621679520208 :: Nat) = a6989586621679520207 <=? a6989586621679520208
type Apply ((^@#@$$) a6989586621679519847 :: TyFun Nat Nat -> Type) (a6989586621679519848 :: Nat) Source #
Instance details Defined in GHC.TypeLits.Singletons.Internal type Apply ((^@#@$$) a6989586621679519847 :: TyFun Nat Nat -> Type) (a6989586621679519848 :: Nat) = a6989586621679519847 ^ a6989586621679519848
type Apply (DivSym1 a6989586621679529054 :: TyFun Nat Nat -> Type) (a6989586621679529055 :: Nat) Source #
Instance details Defined in GHC.TypeLits.Singletons type Apply (DivSym1 a6989586621679529054 :: TyFun Nat Nat -> Type) (a6989586621679529055 :: Nat) = Div a6989586621679529054 a6989586621679529055
type Apply (ModSym1 a6989586621679529457 :: TyFun Nat Nat -> Type) (a6989586621679529458 :: Nat) Source #
Instance details Defined in GHC.TypeLits.Singletons type Apply (ModSym1 a6989586621679529457 :: TyFun Nat Nat -> Type) (a6989586621679529458 :: Nat) = Mod a6989586621679529457 a6989586621679529458
type Apply (QuotSym1 a6989586621679530000 :: TyFun Nat Nat -> Type) (a6989586621679530001 :: Nat) Source #
Instance details Defined in GHC.TypeLits.Singletons type Apply (QuotSym1 a6989586621679530000 :: TyFun Nat Nat -> Type) (a6989586621679530001 :: Nat) = Quot a6989586621679530000 a6989586621679530001
type Apply (RemSym1 a6989586621679529989 :: TyFun Nat Nat -> Type) (a6989586621679529990 :: Nat) Source #
Instance details Defined in GHC.TypeLits.Singletons type Apply (RemSym1 a6989586621679529989 :: TyFun Nat Nat -> Type) (a6989586621679529990 :: Nat) = Rem a6989586621679529989 a6989586621679529990
type Apply (FromIntegerSym0 :: TyFun Nat k2 -> Type) (a6989586621679550152 :: Nat) Source #
Instance details Defined in GHC.Num.Singletons type Apply (FromIntegerSym0 :: TyFun Nat k2 -> Type) (a6989586621679550152 :: Nat) = FromInteger a6989586621679550152 :: k2
type Apply (ToEnumSym0 :: TyFun Nat k2 -> Type) (a6989586621679573385 :: Nat) Source #
Instance details Defined in Data.Singletons.Base.Enum type Apply (ToEnumSym0 :: TyFun Nat k2 -> Type) (a6989586621679573385 :: Nat) = ToEnum a6989586621679573385 :: k2
type Apply (FromEnumSym0 :: TyFun a Nat -> Type) (a6989586621679573388 :: a) Source #
Instance details Defined in Data.Singletons.Base.Enum type Apply (FromEnumSym0 :: TyFun a Nat -> Type) (a6989586621679573388 :: a) = FromEnum a6989586621679573388
type Apply ((!!@#@$$) a6989586621679814074 :: TyFun Nat a -> Type) (a6989586621679814075 :: Nat) Source #
Instance details Defined in Data.List.Singletons.Internal type Apply ((!!@#@$$) a6989586621679814074 :: TyFun Nat a -> Type) (a6989586621679814075 :: Nat) = a6989586621679814074 !! a6989586621679814075
type Apply ((!!@#@$$) a6989586621681120418 :: TyFun Nat a -> Type) (a6989586621681120419 :: Nat) Source #
Instance details Defined in Data.List.NonEmpty.Singletons type Apply ((!!@#@$$) a6989586621681120418 :: TyFun Nat a -> Type) (a6989586621681120419 :: Nat) = a6989586621681120418 !! a6989586621681120419
type Apply (<=?@#@$) (a6989586621679520207 :: Nat) Source #
Instance details Defined in GHC.TypeLits.Singletons.Internal type Apply (<=?@#@$) (a6989586621679520207 :: Nat) = (<=?@#@$$) a6989586621679520207
type Apply (^@#@$) (a6989586621679519847 :: Nat) Source #
Instance details Defined in GHC.TypeLits.Singletons.Internal type Apply (^@#@$) (a6989586621679519847 :: Nat) = (^@#@$$) a6989586621679519847
type Apply DivSym0 (a6989586621679529054 :: Nat) Source #
Instance details Defined in GHC.TypeLits.Singletons type Apply DivSym0 (a6989586621679529054 :: Nat) = DivSym1 a6989586621679529054
type Apply ModSym0 (a6989586621679529457 :: Nat) Source #
Instance details Defined in GHC.TypeLits.Singletons type Apply ModSym0 (a6989586621679529457 :: Nat) = ModSym1 a6989586621679529457
type Apply QuotSym0 (a6989586621679530000 :: Nat) Source #
Instance details Defined in GHC.TypeLits.Singletons type Apply QuotSym0 (a6989586621679530000 :: Nat) = QuotSym1 a6989586621679530000
type Apply RemSym0 (a6989586621679529989 :: Nat) Source #
Instance details Defined in GHC.TypeLits.Singletons type Apply RemSym0 (a6989586621679529989 :: Nat) = RemSym1 a6989586621679529989
type Apply DivModSym0 (a6989586621679530018 :: Nat) Source #
Instance details Defined in GHC.TypeLits.Singletons type Apply DivModSym0 (a6989586621679530018 :: Nat) = DivModSym1 a6989586621679530018
type Apply QuotRemSym0 (a6989586621679530011 :: Nat) Source #
Instance details Defined in GHC.TypeLits.Singletons type Apply QuotRemSym0 (a6989586621679530011 :: Nat) = QuotRemSym1 a6989586621679530011
type Apply (DivModSym1 a6989586621679530018 :: TyFun Nat (Nat, Nat) -> Type) (a6989586621679530019 :: Nat) Source #
Instance details Defined in GHC.TypeLits.Singletons type Apply (DivModSym1 a6989586621679530018 :: TyFun Nat (Nat, Nat) -> Type) (a6989586621679530019 :: Nat) = DivMod a6989586621679530018 a6989586621679530019
type Apply (QuotRemSym1 a6989586621679530011 :: TyFun Nat (Nat, Nat) -> Type) (a6989586621679530012 :: Nat) Source #
Instance details Defined in GHC.TypeLits.Singletons type Apply (QuotRemSym1 a6989586621679530011 :: TyFun Nat (Nat, Nat) -> Type) (a6989586621679530012 :: Nat) = QuotRem a6989586621679530011 a6989586621679530012
type Apply (DropSym0 :: TyFun Nat ([a] ~> [a]) -> Type) (a6989586621679814236 :: Nat) Source #
Instance details Defined in Data.List.Singletons.Internal type Apply (DropSym0 :: TyFun Nat ([a] ~> [a]) -> Type) (a6989586621679814236 :: Nat) = DropSym1 a6989586621679814236 :: TyFun [a] [a] -> Type
type Apply (TakeSym0 :: TyFun Nat ([a] ~> [a]) -> Type) (a6989586621679814249 :: Nat) Source #
Instance details Defined in Data.List.Singletons.Internal type Apply (TakeSym0 :: TyFun Nat ([a] ~> [a]) -> Type) (a6989586621679814249 :: Nat) = TakeSym1 a6989586621679814249 :: TyFun [a] [a] -> Type
type Apply (SplitAtSym0 :: TyFun Nat ([a] ~> ([a], [a])) -> Type) (a6989586621679814229 :: Nat) Source #
Instance details Defined in Data.List.Singletons.Internal type Apply (SplitAtSym0 :: TyFun Nat ([a] ~> ([a], [a])) -> Type) (a6989586621679814229 :: Nat) = SplitAtSym1 a6989586621679814229 :: TyFun [a] ([a], [a]) -> Type
type Apply (ReplicateSym0 :: TyFun Nat (a ~> [a]) -> Type) (a6989586621679814094 :: Nat) Source #
Instance details Defined in Data.List.Singletons.Internal type Apply (ReplicateSym0 :: TyFun Nat (a ~> [a]) -> Type) (a6989586621679814094 :: Nat) = ReplicateSym1 a6989586621679814094 :: TyFun a [a] -> Type
type Apply (ShowsPrecSym0 :: TyFun Nat (a ~> (Symbol ~> Symbol)) -> Type) (a6989586621680196507 :: Nat) Source #
Instance details Defined in Text.Show.Singletons type Apply (ShowsPrecSym0 :: TyFun Nat (a ~> (Symbol ~> Symbol)) -> Type) (a6989586621680196507 :: Nat) = ShowsPrecSym1 a6989586621680196507 :: TyFun a (Symbol ~> Symbol) -> Type
type Apply (TakeSym0 :: TyFun Nat (NonEmpty a ~> [a]) -> Type) (a6989586621681120628 :: Nat) Source #
Instance details Defined in Data.List.NonEmpty.Singletons type Apply (TakeSym0 :: TyFun Nat (NonEmpty a ~> [a]) -> Type) (a6989586621681120628 :: Nat) = TakeSym1 a6989586621681120628 :: TyFun (NonEmpty a) [a] -> Type
type Apply (DropSym0 :: TyFun Nat (NonEmpty a ~> [a]) -> Type) (a6989586621681120619 :: Nat) Source #
Instance details Defined in Data.List.NonEmpty.Singletons type Apply (DropSym0 :: TyFun Nat (NonEmpty a ~> [a]) -> Type) (a6989586621681120619 :: Nat) = DropSym1 a6989586621681120619 :: TyFun (NonEmpty a) [a] -> Type
type Apply (SplitAtSym0 :: TyFun Nat (NonEmpty a ~> ([a], [a])) -> Type) (a6989586621681120610 :: Nat) Source #
Instance details Defined in Data.List.NonEmpty.Singletons type Apply (SplitAtSym0 :: TyFun Nat (NonEmpty a ~> ([a], [a])) -> Type) (a6989586621681120610 :: Nat) = SplitAtSym1 a6989586621681120610 :: TyFun (NonEmpty a) ([a], [a]) -> Type
type Apply (ElemIndicesSym0 :: TyFun a ([a] ~> [Nat]) -> Type) (a6989586621679814441 :: a) Source #
Instance details Defined in Data.List.Singletons.Internal type Apply (ElemIndicesSym0 :: TyFun a ([a] ~> [Nat]) -> Type) (a6989586621679814441 :: a) = ElemIndicesSym1 a6989586621679814441
type Apply (ElemIndexSym0 :: TyFun a ([a] ~> Maybe Nat) -> Type) (a6989586621679814450 :: a) Source #
Instance details Defined in Data.List.Singletons.Internal type Apply (ElemIndexSym0 :: TyFun a ([a] ~> Maybe Nat) -> Type) (a6989586621679814450 :: a) = ElemIndexSym1 a6989586621679814450
type Apply (ReplicateM_Sym0 :: TyFun Nat (m a ~> m ()) -> Type) (a6989586621681234778 :: Nat) Source #
Instance details Defined in Control.Monad.Singletons type Apply (ReplicateM_Sym0 :: TyFun Nat (m a ~> m ()) -> Type) (a6989586621681234778 :: Nat) = ReplicateM_Sym1 a6989586621681234778 :: TyFun (m a) (m ()) -> Type
type Apply (ReplicateMSym0 :: TyFun Nat (m a ~> m [a]) -> Type) (a6989586621681234796 :: Nat) Source #
Instance details Defined in Control.Monad.Singletons type Apply (ReplicateMSym0 :: TyFun Nat (m a ~> m [a]) -> Type) (a6989586621681234796 :: Nat) = ReplicateMSym1 a6989586621681234796 :: TyFun (m a) (m [a]) -> Type
type Apply (LengthSym0 :: TyFun (NonEmpty a) Nat -> Type) (a6989586621681120843 :: NonEmpty a) Source #
Instance details Defined in Data.List.NonEmpty.Singletons type Apply (LengthSym0 :: TyFun (NonEmpty a) Nat -> Type) (a6989586621681120843 :: NonEmpty a) = Length a6989586621681120843
type Apply (LengthSym0 :: TyFun (t a) Nat -> Type) (a6989586621680367327 :: t a) Source #
Instance details Defined in Data.Foldable.Singletons type Apply (LengthSym0 :: TyFun (t a) Nat -> Type) (a6989586621680367327 :: t a) = Length a6989586621680367327
type Apply (FindIndicesSym1 a6989586621679814409 :: TyFun [a] [Nat] -> Type) (a6989586621679814410 :: [a]) Source #
Instance details Defined in Data.List.Singletons.Internal type Apply (FindIndicesSym1 a6989586621679814409 :: TyFun [a] [Nat] -> Type) (a6989586621679814410 :: [a]) = FindIndices a6989586621679814409 a6989586621679814410
type Apply (ElemIndicesSym1 a6989586621679814441 :: TyFun [a] [Nat] -> Type) (a6989586621679814442 :: [a]) Source #
Instance details Defined in Data.List.Singletons.Internal type Apply (ElemIndicesSym1 a6989586621679814441 :: TyFun [a] [Nat] -> Type) (a6989586621679814442 :: [a]) = ElemIndices a6989586621679814441 a6989586621679814442
type Apply (FindIndexSym1 a6989586621679814432 :: TyFun [a] (Maybe Nat) -> Type) (a6989586621679814433 :: [a]) Source #
Instance details Defined in Data.List.Singletons.Internal type Apply (FindIndexSym1 a6989586621679814432 :: TyFun [a] (Maybe Nat) -> Type) (a6989586621679814433 :: [a]) = FindIndex a6989586621679814432 a6989586621679814433
type Apply (ElemIndexSym1 a6989586621679814450 :: TyFun [a] (Maybe Nat) -> Type) (a6989586621679814451 :: [a]) Source #
Instance details Defined in Data.List.Singletons.Internal type Apply (ElemIndexSym1 a6989586621679814450 :: TyFun [a] (Maybe Nat) -> Type) (a6989586621679814451 :: [a]) = ElemIndex a6989586621679814450 a6989586621679814451
type Apply ((!!@#@$) :: TyFun [a] (Nat ~> a) -> Type) (a6989586621679814074 :: [a]) Source #
Instance details Defined in Data.List.Singletons.Internal type Apply ((!!@#@$) :: TyFun [a] (Nat ~> a) -> Type) (a6989586621679814074 :: [a]) = (!!@#@$$) a6989586621679814074
type Apply ((!!@#@$) :: TyFun (NonEmpty a) (Nat ~> a) -> Type) (a6989586621681120418 :: NonEmpty a) Source #
Instance details Defined in Data.List.NonEmpty.Singletons type Apply ((!!@#@$) :: TyFun (NonEmpty a) (Nat ~> a) -> Type) (a6989586621681120418 :: NonEmpty a) = (!!@#@$$) a6989586621681120418
type Apply (FindIndicesSym0 :: TyFun (a ~> Bool) ([a] ~> [Nat]) -> Type) (a6989586621679814409 :: a ~> Bool) Source #
Instance details Defined in Data.List.Singletons.Internal type Apply (FindIndicesSym0 :: TyFun (a ~> Bool) ([a] ~> [Nat]) -> Type) (a6989586621679814409 :: a ~> Bool) = FindIndicesSym1 a6989586621679814409
type Apply (FindIndexSym0 :: TyFun (a ~> Bool) ([a] ~> Maybe Nat) -> Type) (a6989586621679814432 :: a ~> Bool) Source #
Instance details Defined in Data.List.Singletons.Internal type Apply (FindIndexSym0 :: TyFun (a ~> Bool) ([a] ~> Maybe Nat) -> Type) (a6989586621679814432 :: a ~> Bool) = FindIndexSym1 a6989586621679814432

data Symbol #

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

Instances

Instances details

Eq Symbol Source #	This bogus instance is helpful for people who want to define functions over Symbols that will only be used at the type level or as singletons.
Instance details Defined in GHC.TypeLits.Singletons Methods (==) :: Symbol -> Symbol -> Bool # (/=) :: Symbol -> Symbol -> Bool #
Ord Symbol Source #
Instance details Defined in GHC.TypeLits.Singletons 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 Source #
Instance details Defined in GHC.TypeLits.Singletons Methods showsPrec :: Int -> Symbol -> ShowS # show :: Symbol -> String # showList :: [Symbol] -> ShowS #
IsString Symbol Source #
Instance details Defined in GHC.TypeLits.Singletons Methods fromString :: String -> Symbol #
Semigroup Symbol Source #
Instance details Defined in GHC.TypeLits.Singletons Methods (<>) :: Symbol -> Symbol -> Symbol # sconcat :: NonEmpty Symbol -> Symbol # stimes :: Integral b => b -> Symbol -> Symbol #
Monoid Symbol Source #
Instance details Defined in GHC.TypeLits.Singletons Methods mempty :: Symbol # mappend :: Symbol -> Symbol -> Symbol # mconcat :: [Symbol] -> Symbol #
SDecide Symbol Source #
Instance details Defined in GHC.TypeLits.Singletons.Internal Methods (%~) :: forall (a :: Symbol) (b :: Symbol). Sing a -> Sing b -> Decision (a :~: b) #
SingKind Symbol Source #
Instance details Defined in GHC.TypeLits.Singletons.Internal Associated Types type Demote Symbol = (r :: Type) # Methods fromSing :: forall (a :: Symbol). Sing a -> Demote Symbol # toSing :: Demote Symbol -> SomeSing Symbol #
SingKind PErrorMessage Source #
Instance details Defined in Data.Singletons.Base.TypeError Associated Types type Demote PErrorMessage = (r :: Type) # Methods fromSing :: forall (a :: PErrorMessage). Sing a -> Demote PErrorMessage # toSing :: Demote PErrorMessage -> SomeSing PErrorMessage #
SingKind Symbol	Since: base-4.9.0.0
Instance details Defined in GHC.Generics Associated Types type DemoteRep Symbol Methods fromSing :: forall (a :: Symbol). Sing a -> DemoteRep Symbol
SEq Symbol Source #
Instance details Defined in GHC.TypeLits.Singletons.Internal Methods (%==) :: 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 #
PEq Symbol Source #
Instance details Defined in GHC.TypeLits.Singletons.Internal Associated Types type arg == arg :: Bool Source # type arg /= arg :: Bool Source #
SOrd Symbol Source #
Instance details Defined in GHC.TypeLits.Singletons.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 GHC.TypeLits.Singletons.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.Semigroup.Singletons.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.Semigroup.Singletons.Internal Associated Types type arg <> arg :: a Source # type Sconcat arg :: a Source #
SShow Symbol Source #
Instance details Defined in Text.Show.Singletons 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 Text.Show.Singletons 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.Monoid.Singletons 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.Monoid.Singletons 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.String.Singletons Methods sFromString :: forall (t :: Symbol). Sing t -> Sing (Apply FromStringSym0 t) Source #
PIsString Symbol Source #
Instance details Defined in Data.String.Singletons Associated Types type FromString arg :: a Source #
KnownSymbol n => SingI (n :: Symbol) Source #
Instance details Defined in GHC.TypeLits.Singletons.Internal Methods sing :: Sing n #
KnownSymbol a => SingI (a :: Symbol)	Since: base-4.9.0.0
Instance details Defined in GHC.Generics Methods sing :: Sing a
SingI t => SingI ('Text t :: ErrorMessage' Symbol) Source #
Instance details Defined in Data.Singletons.Base.TypeError Methods sing :: Sing ('Text t) #
SingI ty => SingI ('ShowType ty :: ErrorMessage' Symbol) Source #
Instance details Defined in Data.Singletons.Base.TypeError Methods sing :: Sing ('ShowType ty) #
(SingI e1, SingI e2) => SingI (e1 :<>: e2 :: ErrorMessage' Symbol) Source #
Instance details Defined in Data.Singletons.Base.TypeError Methods sing :: Sing (e1 :<>: e2) #
(SingI e1, SingI e2) => SingI (e1 :$$: e2 :: ErrorMessage' Symbol) Source #
Instance details Defined in Data.Singletons.Base.TypeError Methods sing :: Sing (e1 :$$: e2) #
SingI ShowParenSym0 Source #
Instance details Defined in Text.Show.Singletons Methods sing :: Sing ShowParenSym0 #
SingI UnlinesSym0 Source #
Instance details Defined in Data.List.Singletons.Internal Methods sing :: Sing UnlinesSym0 #
SingI UnwordsSym0 Source #
Instance details Defined in Data.List.Singletons.Internal Methods sing :: Sing UnwordsSym0 #
SingI ShowSpaceSym0 Source #
Instance details Defined in Text.Show.Singletons Methods sing :: Sing ShowSpaceSym0 #
SingI ShowCommaSpaceSym0 Source #
Instance details Defined in Text.Show.Singletons Methods sing :: Sing ShowCommaSpaceSym0 #
SingI ShowCharSym0 Source #
Instance details Defined in Text.Show.Singletons Methods sing :: Sing ShowCharSym0 #
SingI ShowStringSym0 Source #
Instance details Defined in Text.Show.Singletons Methods sing :: Sing ShowStringSym0 #
SuppressUnusedWarnings ShowParenSym0 Source #
Instance details Defined in Text.Show.Singletons Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings UnlinesSym0 Source #
Instance details Defined in Data.List.Singletons.Internal Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings UnwordsSym0 Source #
Instance details Defined in Data.List.Singletons.Internal Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings KnownSymbolSym0 Source #
Instance details Defined in GHC.TypeLits.Singletons Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings ShowSpaceSym0 Source #
Instance details Defined in Text.Show.Singletons Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings ShowCommaSpaceSym0 Source #
Instance details Defined in Text.Show.Singletons Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings ShowCharSym0 Source #
Instance details Defined in Text.Show.Singletons Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings ShowStringSym0 Source #
Instance details Defined in Text.Show.Singletons Methods suppressUnusedWarnings :: () #
SingI (TypeErrorSym0 :: TyFun PErrorMessage a -> Type) Source #
Instance details Defined in Data.Singletons.Base.TypeError Methods sing :: Sing TypeErrorSym0 #
SShow a => SingI (ShowListSym0 :: TyFun [a] (Symbol ~> Symbol) -> Type) Source #
Instance details Defined in Text.Show.Singletons Methods sing :: Sing ShowListSym0 #
SShow a => SingI (ShowsPrecSym0 :: TyFun Nat (a ~> (Symbol ~> Symbol)) -> Type) Source #
Instance details Defined in Text.Show.Singletons Methods sing :: Sing ShowsPrecSym0 #
SingI d => SingI (ShowCharSym1 d :: TyFun Symbol Symbol -> Type) Source #
Instance details Defined in Text.Show.Singletons Methods sing :: Sing (ShowCharSym1 d) #
SingI d => SingI (ShowStringSym1 d :: TyFun Symbol Symbol -> Type) Source #
Instance details Defined in Text.Show.Singletons Methods sing :: Sing (ShowStringSym1 d) #
SIsString a => SingI (FromStringSym0 :: TyFun Symbol a -> Type) Source #
Instance details Defined in Data.String.Singletons Methods sing :: Sing FromStringSym0 #
SingI (TextSym0 :: TyFun Symbol (ErrorMessage' Symbol) -> Type) Source #
Instance details Defined in Data.Singletons.Base.TypeError Methods sing :: Sing TextSym0 #
SShow a => SingI (ShowsSym0 :: TyFun a (Symbol ~> Symbol) -> Type) Source #
Instance details Defined in Text.Show.Singletons Methods sing :: Sing ShowsSym0 #
SShow a => SingI (Show_Sym0 :: TyFun a Symbol -> Type) Source #
Instance details Defined in Text.Show.Singletons Methods sing :: Sing Show_Sym0 #
SingI d => SingI (ShowParenSym1 d :: TyFun (Symbol ~> Symbol) (Symbol ~> Symbol) -> Type) Source #
Instance details Defined in Text.Show.Singletons Methods sing :: Sing (ShowParenSym1 d) #
SingI (ShowListWithSym0 :: TyFun (a ~> (Symbol ~> Symbol)) ([a] ~> (Symbol ~> Symbol)) -> Type) Source #
Instance details Defined in Text.Show.Singletons Methods sing :: Sing ShowListWithSym0 #
SingI ((:$$:@#@$) :: TyFun (ErrorMessage' Symbol) (ErrorMessage' Symbol ~> ErrorMessage' Symbol) -> Type) Source #
Instance details Defined in Data.Singletons.Base.TypeError Methods sing :: Sing (:$$:@#@$) #
SingI ((:<>:@#@$) :: TyFun (ErrorMessage' Symbol) (ErrorMessage' Symbol ~> ErrorMessage' Symbol) -> Type) Source #
Instance details Defined in Data.Singletons.Base.TypeError Methods sing :: Sing (:<>:@#@$) #
SuppressUnusedWarnings (ShowListSym0 :: TyFun [a] (Symbol ~> Symbol) -> Type) Source #
Instance details Defined in Text.Show.Singletons Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (ShowsPrecSym0 :: TyFun Nat (a ~> (Symbol ~> Symbol)) -> Type) Source #
Instance details Defined in Text.Show.Singletons Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (ShowCharSym1 a6989586621680196473 :: TyFun Symbol Symbol -> Type) Source #
Instance details Defined in Text.Show.Singletons Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (ShowStringSym1 a6989586621680196462 :: TyFun Symbol Symbol -> Type) Source #
Instance details Defined in Text.Show.Singletons Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (FromStringSym0 :: TyFun Symbol a -> Type) Source #
Instance details Defined in Data.String.Singletons Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (Show_Sym0 :: TyFun a Symbol -> Type) Source #
Instance details Defined in Text.Show.Singletons Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (ShowsSym0 :: TyFun a (Symbol ~> Symbol) -> Type) Source #
Instance details Defined in Text.Show.Singletons Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (ShowParenSym1 a6989586621680196446 :: TyFun (Symbol ~> Symbol) (Symbol ~> Symbol) -> Type) Source #
Instance details Defined in Text.Show.Singletons Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (ShowListWithSym0 :: TyFun (a ~> (Symbol ~> Symbol)) ([a] ~> (Symbol ~> Symbol)) -> Type) Source #
Instance details Defined in Text.Show.Singletons Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (TypeErrorSym0 :: TyFun PErrorMessage a -> Type) Source #
Instance details Defined in Data.Singletons.Base.TypeError Methods suppressUnusedWarnings :: () #
SingI d => SingI (ShowListWithSym1 d :: TyFun [a] (Symbol ~> Symbol) -> Type) Source #
Instance details Defined in Text.Show.Singletons Methods sing :: Sing (ShowListWithSym1 d) #
(SShow a, SingI d) => SingI (ShowListSym1 d :: TyFun Symbol Symbol -> Type) Source #
Instance details Defined in Text.Show.Singletons Methods sing :: Sing (ShowListSym1 d) #
(SShow a, SingI d) => SingI (ShowsSym1 d :: TyFun Symbol Symbol -> Type) Source #
Instance details Defined in Text.Show.Singletons Methods sing :: Sing (ShowsSym1 d) #
(SingI d1, SingI d2) => SingI (ShowParenSym2 d1 d2 :: TyFun Symbol Symbol -> Type) Source #
Instance details Defined in Text.Show.Singletons Methods sing :: Sing (ShowParenSym2 d1 d2) #
SingI (ErrorSym0 :: TyFun Symbol a -> Type) Source #
Instance details Defined in GHC.TypeLits.Singletons.Internal Methods sing :: Sing ErrorSym0 #
SingI (ErrorWithoutStackTraceSym0 :: TyFun Symbol a -> Type) Source #
Instance details Defined in GHC.TypeLits.Singletons.Internal Methods sing :: Sing ErrorWithoutStackTraceSym0 #
SingI (ShowTypeSym0 :: TyFun t (ErrorMessage' Symbol) -> Type) Source #
Instance details Defined in Data.Singletons.Base.TypeError Methods sing :: Sing ShowTypeSym0 #
(SShow a, SingI d) => SingI (ShowsPrecSym1 d :: TyFun a (Symbol ~> Symbol) -> Type) Source #
Instance details Defined in Text.Show.Singletons Methods sing :: Sing (ShowsPrecSym1 d) #
SingI x => SingI ((:$$:@#@$$) x :: TyFun (ErrorMessage' Symbol) (ErrorMessage' Symbol) -> Type) Source #
Instance details Defined in Data.Singletons.Base.TypeError Methods sing :: Sing ((:$$:@#@$$) x) #
SingI x => SingI ((:<>:@#@$$) x :: TyFun (ErrorMessage' Symbol) (ErrorMessage' Symbol) -> Type) Source #
Instance details Defined in Data.Singletons.Base.TypeError Methods sing :: Sing ((:<>:@#@$$) x) #
SuppressUnusedWarnings (ShowListWithSym1 a6989586621680196481 :: TyFun [a] (Symbol ~> Symbol) -> Type) Source #
Instance details Defined in Text.Show.Singletons Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (ShowListSym1 a6989586621680196516 :: TyFun Symbol Symbol -> Type) Source #
Instance details Defined in Text.Show.Singletons Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (ShowsSym1 a6989586621680196499 :: TyFun Symbol Symbol -> Type) Source #
Instance details Defined in Text.Show.Singletons Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (ShowParenSym2 a6989586621680196446 a6989586621680196447 :: TyFun Symbol Symbol -> Type) Source #
Instance details Defined in Text.Show.Singletons Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (ShowsPrecSym1 a6989586621680196507 :: TyFun a (Symbol ~> Symbol) -> Type) Source #
Instance details Defined in Text.Show.Singletons Methods suppressUnusedWarnings :: () #
(SShow a, SingI d1, SingI d2) => SingI (ShowsPrecSym2 d1 d2 :: TyFun Symbol Symbol -> Type) Source #
Instance details Defined in Text.Show.Singletons Methods sing :: Sing (ShowsPrecSym2 d1 d2) #
(SingI d1, SingI d2) => SingI (ShowListWithSym2 d1 d2 :: TyFun Symbol Symbol -> Type) Source #
Instance details Defined in Text.Show.Singletons Methods sing :: Sing (ShowListWithSym2 d1 d2) #
SuppressUnusedWarnings (ShowsPrecSym2 a6989586621680196507 a6989586621680196508 :: TyFun Symbol Symbol -> Type) Source #
Instance details Defined in Text.Show.Singletons Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (ShowListWithSym2 a6989586621680196481 a6989586621680196482 :: TyFun Symbol Symbol -> Type) Source #
Instance details Defined in Text.Show.Singletons Methods suppressUnusedWarnings :: () #
type Sing Source #
Instance details Defined in GHC.TypeLits.Singletons.Internal type Sing = SSymbol
type Sing Source #
Instance details Defined in Data.Singletons.Base.TypeError type Sing = SErrorMessage
type Demote Symbol Source #
Instance details Defined in GHC.TypeLits.Singletons.Internal type Demote Symbol = Text
type Demote PErrorMessage Source #
Instance details Defined in Data.Singletons.Base.TypeError type Demote PErrorMessage = ErrorMessage
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.Monoid.Singletons type Mempty
type Sconcat (arg :: NonEmpty Symbol) Source #
Instance details Defined in Data.Semigroup.Singletons.Internal type Sconcat (arg :: NonEmpty Symbol)
type Show_ (arg :: Symbol) Source #
Instance details Defined in Text.Show.Singletons type Show_ (arg :: Symbol)
type Mconcat (arg :: [Symbol]) Source #
Instance details Defined in Data.Monoid.Singletons type Mconcat (arg :: [Symbol])
type FromString a Source #
Instance details Defined in Data.String.Singletons type FromString a = a
type (x :: Symbol) == (y :: Symbol) Source #
Instance details Defined in GHC.TypeLits.Singletons.Internal type (x :: Symbol) == (y :: Symbol) = DefaultEq x y
type (arg1 :: Symbol) /= (arg2 :: Symbol) Source #
Instance details Defined in GHC.TypeLits.Singletons.Internal type (arg1 :: Symbol) /= (arg2 :: Symbol)
type Compare (a :: Symbol) (b :: Symbol) Source #
Instance details Defined in GHC.TypeLits.Singletons.Internal type Compare (a :: Symbol) (b :: Symbol) = CmpSymbol a b
type (arg1 :: Symbol) < (arg2 :: Symbol) Source #
Instance details Defined in GHC.TypeLits.Singletons.Internal type (arg1 :: Symbol) < (arg2 :: Symbol)
type (arg1 :: Symbol) <= (arg2 :: Symbol) Source #
Instance details Defined in GHC.TypeLits.Singletons.Internal type (arg1 :: Symbol) <= (arg2 :: Symbol)
type (arg1 :: Symbol) > (arg2 :: Symbol) Source #
Instance details Defined in GHC.TypeLits.Singletons.Internal type (arg1 :: Symbol) > (arg2 :: Symbol)
type (arg1 :: Symbol) >= (arg2 :: Symbol) Source #
Instance details Defined in GHC.TypeLits.Singletons.Internal type (arg1 :: Symbol) >= (arg2 :: Symbol)
type Max (arg1 :: Symbol) (arg2 :: Symbol) Source #
Instance details Defined in GHC.TypeLits.Singletons.Internal type Max (arg1 :: Symbol) (arg2 :: Symbol)
type Min (arg1 :: Symbol) (arg2 :: Symbol) Source #
Instance details Defined in GHC.TypeLits.Singletons.Internal type Min (arg1 :: Symbol) (arg2 :: Symbol)
type (a :: Symbol) <> (b :: Symbol) Source #
Instance details Defined in Data.Semigroup.Singletons.Internal type (a :: Symbol) <> (b :: Symbol) = AppendSymbol a b
type ShowList (arg1 :: [Symbol]) arg2 Source #
Instance details Defined in Text.Show.Singletons type ShowList (arg1 :: [Symbol]) arg2
type Mappend (arg1 :: Symbol) (arg2 :: Symbol) Source #
Instance details Defined in Data.Monoid.Singletons type Mappend (arg1 :: Symbol) (arg2 :: Symbol)
type Apply KnownSymbolSym0 (a6989586621679528271 :: Symbol) Source #
Instance details Defined in GHC.TypeLits.Singletons type Apply KnownSymbolSym0 (a6989586621679528271 :: Symbol) = KnownSymbol a6989586621679528271
type Apply ShowSpaceSym0 (a6989586621680196434 :: Symbol) Source #
Instance details Defined in Text.Show.Singletons type Apply ShowSpaceSym0 (a6989586621680196434 :: Symbol) = ShowSpace a6989586621680196434
type Apply ShowCommaSpaceSym0 (a6989586621680196428 :: Symbol) Source #
Instance details Defined in Text.Show.Singletons type Apply ShowCommaSpaceSym0 (a6989586621680196428 :: Symbol) = ShowCommaSpace a6989586621680196428
type ShowsPrec a1 (a2 :: Symbol) a3 Source #
Instance details Defined in Text.Show.Singletons type ShowsPrec a1 (a2 :: Symbol) a3
type Apply (ShowCharSym1 a6989586621680196473 :: TyFun Symbol Symbol -> Type) (a6989586621680196474 :: Symbol) Source #
Instance details Defined in Text.Show.Singletons type Apply (ShowCharSym1 a6989586621680196473 :: TyFun Symbol Symbol -> Type) (a6989586621680196474 :: Symbol) = ShowChar a6989586621680196473 a6989586621680196474
type Apply (ShowStringSym1 a6989586621680196462 :: TyFun Symbol Symbol -> Type) (a6989586621680196463 :: Symbol) Source #
Instance details Defined in Text.Show.Singletons type Apply (ShowStringSym1 a6989586621680196462 :: TyFun Symbol Symbol -> Type) (a6989586621680196463 :: Symbol) = ShowString a6989586621680196462 a6989586621680196463
type Apply (FromStringSym0 :: TyFun Symbol k2 -> Type) (a6989586621681219672 :: Symbol) Source #
Instance details Defined in Data.String.Singletons type Apply (FromStringSym0 :: TyFun Symbol k2 -> Type) (a6989586621681219672 :: Symbol) = FromString a6989586621681219672 :: k2
type Apply (Show_Sym0 :: TyFun a Symbol -> Type) (a6989586621680196512 :: a) Source #
Instance details Defined in Text.Show.Singletons type Apply (Show_Sym0 :: TyFun a Symbol -> Type) (a6989586621680196512 :: a) = Show_ a6989586621680196512
type Apply (TypeErrorSym0 :: TyFun PErrorMessage k2 -> Type) (a6989586621679646232 :: PErrorMessage) Source #
Instance details Defined in Data.Singletons.Base.TypeError type Apply (TypeErrorSym0 :: TyFun PErrorMessage k2 -> Type) (a6989586621679646232 :: PErrorMessage) = TypeError a6989586621679646232 :: k2
type Apply (ShowListSym1 a6989586621680196516 :: TyFun Symbol Symbol -> Type) (a6989586621680196517 :: Symbol) Source #
Instance details Defined in Text.Show.Singletons type Apply (ShowListSym1 a6989586621680196516 :: TyFun Symbol Symbol -> Type) (a6989586621680196517 :: Symbol) = ShowList a6989586621680196516 a6989586621680196517
type Apply (ShowsSym1 a6989586621680196499 :: TyFun Symbol Symbol -> Type) (a6989586621680196500 :: Symbol) Source #
Instance details Defined in Text.Show.Singletons type Apply (ShowsSym1 a6989586621680196499 :: TyFun Symbol Symbol -> Type) (a6989586621680196500 :: Symbol) = Shows a6989586621680196499 a6989586621680196500
type Apply (ShowParenSym2 a6989586621680196446 a6989586621680196447 :: TyFun Symbol Symbol -> Type) (a6989586621680196448 :: Symbol) Source #
Instance details Defined in Text.Show.Singletons type Apply (ShowParenSym2 a6989586621680196446 a6989586621680196447 :: TyFun Symbol Symbol -> Type) (a6989586621680196448 :: Symbol) = ShowParen a6989586621680196446 a6989586621680196447 a6989586621680196448
type Apply (ShowsPrecSym2 a6989586621680196507 a6989586621680196508 :: TyFun Symbol Symbol -> Type) (a6989586621680196509 :: Symbol) Source #
Instance details Defined in Text.Show.Singletons type Apply (ShowsPrecSym2 a6989586621680196507 a6989586621680196508 :: TyFun Symbol Symbol -> Type) (a6989586621680196509 :: Symbol) = ShowsPrec a6989586621680196507 a6989586621680196508 a6989586621680196509
type Apply (ShowListWithSym2 a6989586621680196481 a6989586621680196482 :: TyFun Symbol Symbol -> Type) (a6989586621680196483 :: Symbol) Source #
Instance details Defined in Text.Show.Singletons type Apply (ShowListWithSym2 a6989586621680196481 a6989586621680196482 :: TyFun Symbol Symbol -> Type) (a6989586621680196483 :: Symbol) = ShowListWith a6989586621680196481 a6989586621680196482 a6989586621680196483
type Apply ShowParenSym0 (a6989586621680196446 :: Bool) Source #
Instance details Defined in Text.Show.Singletons type Apply ShowParenSym0 (a6989586621680196446 :: Bool) = ShowParenSym1 a6989586621680196446
type Apply ShowCharSym0 (a6989586621680196473 :: Symbol) Source #
Instance details Defined in Text.Show.Singletons type Apply ShowCharSym0 (a6989586621680196473 :: Symbol) = ShowCharSym1 a6989586621680196473
type Apply ShowStringSym0 (a6989586621680196462 :: Symbol) Source #
Instance details Defined in Text.Show.Singletons type Apply ShowStringSym0 (a6989586621680196462 :: Symbol) = ShowStringSym1 a6989586621680196462
type Apply (ShowsPrecSym0 :: TyFun Nat (a ~> (Symbol ~> Symbol)) -> Type) (a6989586621680196507 :: Nat) Source #
Instance details Defined in Text.Show.Singletons type Apply (ShowsPrecSym0 :: TyFun Nat (a ~> (Symbol ~> Symbol)) -> Type) (a6989586621680196507 :: Nat) = ShowsPrecSym1 a6989586621680196507 :: TyFun a (Symbol ~> Symbol) -> Type
type Apply (ShowsSym0 :: TyFun a (Symbol ~> Symbol) -> Type) (a6989586621680196499 :: a) Source #
Instance details Defined in Text.Show.Singletons type Apply (ShowsSym0 :: TyFun a (Symbol ~> Symbol) -> Type) (a6989586621680196499 :: a) = ShowsSym1 a6989586621680196499
type Apply (ShowsPrecSym1 a6989586621680196507 :: TyFun a (Symbol ~> Symbol) -> Type) (a6989586621680196508 :: a) Source #
Instance details Defined in Text.Show.Singletons type Apply (ShowsPrecSym1 a6989586621680196507 :: TyFun a (Symbol ~> Symbol) -> Type) (a6989586621680196508 :: a) = ShowsPrecSym2 a6989586621680196507 a6989586621680196508
type Apply UnlinesSym0 (a6989586621679814611 :: [Symbol]) Source #
Instance details Defined in Data.List.Singletons.Internal type Apply UnlinesSym0 (a6989586621679814611 :: [Symbol]) = Unlines a6989586621679814611
type Apply UnwordsSym0 (a6989586621679814601 :: [Symbol]) Source #
Instance details Defined in Data.List.Singletons.Internal type Apply UnwordsSym0 (a6989586621679814601 :: [Symbol]) = Unwords a6989586621679814601
type Apply (ShowListSym0 :: TyFun [a] (Symbol ~> Symbol) -> Type) (a6989586621680196516 :: [a]) Source #
Instance details Defined in Text.Show.Singletons type Apply (ShowListSym0 :: TyFun [a] (Symbol ~> Symbol) -> Type) (a6989586621680196516 :: [a]) = ShowListSym1 a6989586621680196516
type Apply (ShowListWithSym1 a6989586621680196481 :: TyFun [a] (Symbol ~> Symbol) -> Type) (a6989586621680196482 :: [a]) Source #
Instance details Defined in Text.Show.Singletons type Apply (ShowListWithSym1 a6989586621680196481 :: TyFun [a] (Symbol ~> Symbol) -> Type) (a6989586621680196482 :: [a]) = ShowListWithSym2 a6989586621680196481 a6989586621680196482
type Apply (ShowParenSym1 a6989586621680196446 :: TyFun (Symbol ~> Symbol) (Symbol ~> Symbol) -> Type) (a6989586621680196447 :: Symbol ~> Symbol) Source #
Instance details Defined in Text.Show.Singletons type Apply (ShowParenSym1 a6989586621680196446 :: TyFun (Symbol ~> Symbol) (Symbol ~> Symbol) -> Type) (a6989586621680196447 :: Symbol ~> Symbol) = ShowParenSym2 a6989586621680196446 a6989586621680196447
type Apply (ShowListWithSym0 :: TyFun (a ~> (Symbol ~> Symbol)) ([a] ~> (Symbol ~> Symbol)) -> Type) (a6989586621680196481 :: a ~> (Symbol ~> Symbol)) Source #
Instance details Defined in Text.Show.Singletons type Apply (ShowListWithSym0 :: TyFun (a ~> (Symbol ~> Symbol)) ([a] ~> (Symbol ~> Symbol)) -> Type) (a6989586621680196481 :: a ~> (Symbol ~> Symbol)) = ShowListWithSym1 a6989586621680196481

type family Sing :: k -> Type #

The singleton kind-indexed type family.

Instances

Instances details

type Sing Source #
Instance details Defined in Data.Singletons.Base.Instances type Sing = SBool
type Sing Source #
Instance details Defined in Data.Singletons.Base.Instances type Sing = SOrdering
type Sing Source #
Instance details Defined in GHC.TypeLits.Singletons.Internal type Sing = SNat
type Sing Source #
Instance details Defined in GHC.TypeLits.Singletons.Internal type Sing = SSymbol
type Sing Source #
Instance details Defined in Data.Singletons.Base.Instances type Sing = STuple0
type Sing Source #
Instance details Defined in Data.Singletons.Base.Instances type Sing = SVoid
type Sing Source #
Instance details Defined in Data.Semigroup.Singletons.Internal type Sing = SAll
type Sing Source #
Instance details Defined in Data.Semigroup.Singletons.Internal type Sing = SAny
type Sing Source #
Instance details Defined in Data.Singletons.Base.TypeError type Sing = SErrorMessage
type Sing Source #
Instance details Defined in Data.Singletons.Base.Instances type Sing = SList :: [a] -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Base.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.Base.TypeRepTYPE type Sing = TypeRep :: TYPE rep -> Type
type Sing Source #
Instance details Defined in Data.Semigroup.Singletons.Internal type Sing = SMin :: Min a -> Type
type Sing Source #
Instance details Defined in Data.Semigroup.Singletons.Internal type Sing = SMax :: Max a -> Type
type Sing Source #
Instance details Defined in Data.Semigroup.Singletons.Internal type Sing = SFirst :: First a -> Type
type Sing Source #
Instance details Defined in Data.Semigroup.Singletons.Internal type Sing = SLast :: Last a -> Type
type Sing Source #
Instance details Defined in Data.Semigroup.Singletons.Internal type Sing = SWrappedMonoid :: WrappedMonoid m -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Base.Instances type Sing = SIdentity :: Identity a -> Type
type Sing Source #
Instance details Defined in Data.Monoid.Singletons type Sing = SFirst :: First a -> Type
type Sing Source #
Instance details Defined in Data.Monoid.Singletons type Sing = SLast :: Last a -> Type
type Sing Source #
Instance details Defined in Data.Semigroup.Singletons.Internal type Sing = SDual :: Dual a -> Type
type Sing Source #
Instance details Defined in Data.Semigroup.Singletons.Internal type Sing = SSum :: Sum a -> Type
type Sing Source #
Instance details Defined in Data.Semigroup.Singletons.Internal type Sing = SProduct :: Product a -> Type
type Sing Source #
Instance details Defined in Data.Ord.Singletons type Sing = SDown :: Down a -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Base.Instances type Sing = SNonEmpty :: NonEmpty a -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Base.Instances type Sing = SEither :: Either a b -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Base.Instances type Sing = STuple2 :: (a, b) -> Type
type Sing Source #
Instance details Defined in Data.Semigroup.Singletons type Sing = SArg :: Arg a b -> Type
type Sing Source #
Instance details Defined in Data.Proxy.Singletons type Sing = SProxy :: Proxy t -> Type
type Sing
Instance details Defined in Data.Singletons type Sing = SWrappedSing :: WrappedSing a -> Type
type Sing
Instance details Defined in Data.Singletons type Sing = SLambda :: (k1 ~> k2) -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Base.Instances type Sing = STuple3 :: (a, b, c) -> Type
type Sing Source #
Instance details Defined in Data.Functor.Const.Singletons type Sing = SConst :: Const a b -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Base.Instances type Sing = STuple4 :: (a, b, c, d) -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Base.Instances type Sing = STuple5 :: (a, b, c, d, e) -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Base.Instances type Sing = STuple6 :: (a, b, c, d, e, f) -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Base.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) Source #
Instance details Defined in GHC.TypeLits.Singletons.Internal 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) Source #
Instance details Defined in GHC.TypeLits.Singletons.Internal 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) #

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

Since: base-4.7.0.0

Minimal complete definition

natSing

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

Since: base-4.10.0.0

class KnownSymbol (n :: Symbol) #

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

Since: base-4.7.0.0

Minimal complete definition

symbolSing

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

Since: base-4.7.0.0

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

Exponentiation of type-level naturals.

Since: base-4.7.0.0

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

The singleton analogue of (^) for Nats.

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

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

(%<=?) :: Sing a -> Sing b -> Sing (a <=? b) infix 4 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.Ord.Singletons, and not the <= from GHC.TypeNats. The latter is simply a type alias for (a <=? b) ~ 'True.)

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

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

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

Since: base-4.11.0.0

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

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

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

Since: base-4.11.0.0

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

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

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

Since: base-4.11.0.0

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

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

Equations

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

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

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

Equations

Quot a_6989586621679529993 a_6989586621679529995 = Apply (Apply DivSym0 a_6989586621679529993) a_6989586621679529995

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_6989586621679529982 a_6989586621679529984 = Apply (Apply ModSym0 a_6989586621679529982) a_6989586621679529984

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_6989586621679530004 a_6989586621679530006 = Apply (Apply DivModSym0 a_6989586621679530004) a_6989586621679530006

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

Defunctionalization symbols

data ErrorSym0 :: (~>) k0 k Source #

Instances

Instances details

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

type family ErrorSym1 (a6989586621679518606 :: k0) :: k where ... Source #

Equations

ErrorSym1 a6989586621679518606 = Error a6989586621679518606

data ErrorWithoutStackTraceSym0 :: (~>) k0 k Source #

Instances

Instances details

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

type family ErrorWithoutStackTraceSym1 (a6989586621679518903 :: k0) :: k where ... Source #

Equations

ErrorWithoutStackTraceSym1 a6989586621679518903 = ErrorWithoutStackTrace a6989586621679518903

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

Equations

UndefinedSym0 = Undefined

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

Instances

Instances details

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

type family KnownNatSym1 (a6989586621679528269 :: Nat) :: Constraint where ... Source #

Equations

KnownNatSym1 a6989586621679528269 = KnownNat a6989586621679528269

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

Instances

Instances details

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

type family KnownSymbolSym1 (a6989586621679528271 :: Symbol) :: Constraint where ... Source #

Equations

KnownSymbolSym1 a6989586621679528271 = KnownSymbol a6989586621679528271

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

Instances

Instances details

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

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

Instances

Instances details

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

type family (a6989586621679519847 :: Nat) ^@#@$$$ (a6989586621679519848 :: Nat) :: Nat where ... infixr 8 Source #

Equations

a6989586621679519847 ^@#@$$$ a6989586621679519848 = (^) a6989586621679519847 a6989586621679519848

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

Instances

Instances details

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

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

Instances

Instances details

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

type family (a6989586621679520207 :: Nat) <=?@#@$$$ (a6989586621679520208 :: Nat) :: Bool where ... infix 4 Source #

Equations

a6989586621679520207 <=?@#@$$$ a6989586621679520208 = (<=?) a6989586621679520207 a6989586621679520208

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

Instances

Instances details

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

type family Log2Sym1 (a6989586621679528808 :: Nat) :: Nat where ... Source #

Equations

Log2Sym1 a6989586621679528808 = Log2 a6989586621679528808

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

Instances

Instances details

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

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

Instances

Instances details

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

type family DivSym2 (a6989586621679529054 :: Nat) (a6989586621679529055 :: Nat) :: Nat where ... infixl 7 Source #

Equations

DivSym2 a6989586621679529054 a6989586621679529055 = Div a6989586621679529054 a6989586621679529055

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

Instances

Instances details

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

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

Instances

Instances details

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

type family ModSym2 (a6989586621679529457 :: Nat) (a6989586621679529458 :: Nat) :: Nat where ... infixl 7 Source #

Equations

ModSym2 a6989586621679529457 a6989586621679529458 = Mod a6989586621679529457 a6989586621679529458

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

Instances

Instances details

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

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

Instances

Instances details

SuppressUnusedWarnings (DivModSym1 a6989586621679530018 :: TyFun Nat (Nat, Nat) -> Type) Source #
Instance details Defined in GHC.TypeLits.Singletons Methods suppressUnusedWarnings :: () #
type Apply (DivModSym1 a6989586621679530018 :: TyFun Nat (Nat, Nat) -> Type) (a6989586621679530019 :: Nat) Source #
Instance details Defined in GHC.TypeLits.Singletons type Apply (DivModSym1 a6989586621679530018 :: TyFun Nat (Nat, Nat) -> Type) (a6989586621679530019 :: Nat) = DivMod a6989586621679530018 a6989586621679530019

type family DivModSym2 (a6989586621679530018 :: Nat) (a6989586621679530019 :: Nat) :: (Nat, Nat) where ... Source #

Equations

DivModSym2 a6989586621679530018 a6989586621679530019 = DivMod a6989586621679530018 a6989586621679530019

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

Instances

Instances details

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

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

Instances

Instances details

SuppressUnusedWarnings (QuotSym1 a6989586621679530000 :: TyFun Nat Nat -> Type) Source #
Instance details Defined in GHC.TypeLits.Singletons Methods suppressUnusedWarnings :: () #
type Apply (QuotSym1 a6989586621679530000 :: TyFun Nat Nat -> Type) (a6989586621679530001 :: Nat) Source #
Instance details Defined in GHC.TypeLits.Singletons type Apply (QuotSym1 a6989586621679530000 :: TyFun Nat Nat -> Type) (a6989586621679530001 :: Nat) = Quot a6989586621679530000 a6989586621679530001

type family QuotSym2 (a6989586621679530000 :: Nat) (a6989586621679530001 :: Nat) :: Nat where ... infixl 7 Source #

Equations

QuotSym2 a6989586621679530000 a6989586621679530001 = Quot a6989586621679530000 a6989586621679530001

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

Instances

Instances details

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

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

Instances

Instances details

SuppressUnusedWarnings (RemSym1 a6989586621679529989 :: TyFun Nat Nat -> Type) Source #
Instance details Defined in GHC.TypeLits.Singletons Methods suppressUnusedWarnings :: () #
type Apply (RemSym1 a6989586621679529989 :: TyFun Nat Nat -> Type) (a6989586621679529990 :: Nat) Source #
Instance details Defined in GHC.TypeLits.Singletons type Apply (RemSym1 a6989586621679529989 :: TyFun Nat Nat -> Type) (a6989586621679529990 :: Nat) = Rem a6989586621679529989 a6989586621679529990

type family RemSym2 (a6989586621679529989 :: Nat) (a6989586621679529990 :: Nat) :: Nat where ... infixl 7 Source #

Equations

RemSym2 a6989586621679529989 a6989586621679529990 = Rem a6989586621679529989 a6989586621679529990

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

Instances

Instances details

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

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

Instances

Instances details

SuppressUnusedWarnings (QuotRemSym1 a6989586621679530011 :: TyFun Nat (Nat, Nat) -> Type) Source #
Instance details Defined in GHC.TypeLits.Singletons Methods suppressUnusedWarnings :: () #
type Apply (QuotRemSym1 a6989586621679530011 :: TyFun Nat (Nat, Nat) -> Type) (a6989586621679530012 :: Nat) Source #
Instance details Defined in GHC.TypeLits.Singletons type Apply (QuotRemSym1 a6989586621679530011 :: TyFun Nat (Nat, Nat) -> Type) (a6989586621679530012 :: Nat) = QuotRem a6989586621679530011 a6989586621679530012

type family QuotRemSym2 (a6989586621679530011 :: Nat) (a6989586621679530012 :: Nat) :: (Nat, Nat) where ... Source #

Equations

QuotRemSym2 a6989586621679530011 a6989586621679530012 = QuotRem a6989586621679530011 a6989586621679530012

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 #