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

Data.Singletons.TypeLits

Contents

Defunctionalization symbols
Orphan instances

Description

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

Synopsis

data Nat
data Symbol
type family Sing
data SNat n = KnownNat n => SNat
data SSymbol n = KnownSymbol n => SSym
withKnownNat :: Sing n -> (KnownNat n => r) -> r
withKnownSymbol :: Sing n -> (KnownSymbol n => r) -> r
type family Error str where ...
sError :: HasCallStack => Sing (str :: Symbol) -> a
type family ErrorWithoutStackTrace str where ...
sErrorWithoutStackTrace :: Sing (str :: Symbol) -> a
type family Undefined 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 a where ...
sDivMod :: Sing x -> Sing y -> Sing (DivMod x y)
type family Quot a a where ...
sQuot :: Sing x -> Sing y -> Sing (Quot x y)
type family Rem a a where ...
sRem :: Sing x -> Sing y -> Sing (Rem x y)
type family QuotRem a a where ...
sQuotRem :: Sing x -> Sing y -> Sing (QuotRem x y)
data ErrorSym0 a6989586621679472252
type ErrorSym1 (a6989586621679472252 :: k0) = Error a6989586621679472252 :: k
data ErrorWithoutStackTraceSym0 a6989586621679472488
type ErrorWithoutStackTraceSym1 (a6989586621679472488 :: k0) = ErrorWithoutStackTrace a6989586621679472488 :: k
type UndefinedSym0 = Undefined :: k
data KnownNatSym0 a6989586621679491988
type KnownNatSym1 (a6989586621679491988 :: Nat) = KnownNat a6989586621679491988 :: Constraint
data KnownSymbolSym0 a6989586621679491990
type KnownSymbolSym1 (a6989586621679491990 :: Symbol) = KnownSymbol a6989586621679491990 :: Constraint
data (^@#@$) a6989586621679472866
data a6989586621679472866 ^@#@$$ a6989586621679472867
type (^@#@$$$) (a6989586621679472866 :: Nat) (a6989586621679472867 :: Nat) = (^) a6989586621679472866 a6989586621679472867 :: Nat
data (<=?@#@$) a6989586621679473158
data a6989586621679473158 <=?@#@$$ a6989586621679473159
type (<=?@#@$$$) (a6989586621679473158 :: Nat) (a6989586621679473159 :: Nat) = (<=?) a6989586621679473158 a6989586621679473159 :: Bool
data Log2Sym0 a6989586621679492472
type Log2Sym1 (a6989586621679492472 :: Nat) = Log2 a6989586621679492472 :: Nat
data DivSym0 a6989586621679492680
data DivSym1 a6989586621679492680 a6989586621679492681
type DivSym2 (a6989586621679492680 :: Nat) (a6989586621679492681 :: Nat) = Div a6989586621679492680 a6989586621679492681 :: Nat
data ModSym0 a6989586621679493016
data ModSym1 a6989586621679493016 a6989586621679493017
type ModSym2 (a6989586621679493016 :: Nat) (a6989586621679493017 :: Nat) = Mod a6989586621679493016 a6989586621679493017 :: Nat
data DivModSym0 a6989586621679493510
data DivModSym1 a6989586621679493510 a6989586621679493511
type DivModSym2 (a6989586621679493510 :: Nat) (a6989586621679493511 :: Nat) = DivMod a6989586621679493510 a6989586621679493511 :: (Nat, Nat)
data QuotSym0 a6989586621679493492
data QuotSym1 a6989586621679493492 a6989586621679493493
type QuotSym2 (a6989586621679493492 :: Nat) (a6989586621679493493 :: Nat) = Quot a6989586621679493492 a6989586621679493493 :: Nat
data RemSym0 a6989586621679493481
data RemSym1 a6989586621679493481 a6989586621679493482
type RemSym2 (a6989586621679493481 :: Nat) (a6989586621679493482 :: Nat) = Rem a6989586621679493481 a6989586621679493482 :: Nat
data QuotRemSym0 a6989586621679493503
data QuotRemSym1 a6989586621679493503 a6989586621679493504
type QuotRemSym2 (a6989586621679493503 :: Nat) (a6989586621679493504 :: Nat) = QuotRem a6989586621679493503 a6989586621679493504 :: (Nat, Nat)

Documentation

data Nat #

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

Instances

Instances details

Enum Nat Source #
Instance details Defined in Data.Singletons.TypeLits Methods succ :: Nat -> Nat # pred :: Nat -> Nat # toEnum :: Int -> Nat # fromEnum :: Nat -> Int # enumFrom :: Nat -> [Nat] # enumFromThen :: Nat -> Nat -> [Nat] # enumFromTo :: Nat -> Nat -> [Nat] # enumFromThenTo :: Nat -> Nat -> Nat -> [Nat] #
Eq Nat Source #
Instance details Defined in Data.Singletons.TypeLits 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 Data.Singletons.TypeLits Methods (+) :: Nat -> Nat -> Nat # (-) :: Nat -> Nat -> Nat # (*) :: Nat -> Nat -> Nat # negate :: Nat -> Nat # abs :: Nat -> Nat # signum :: Nat -> Nat # fromInteger :: Integer -> Nat #
Ord Nat Source #
Instance details Defined in Data.Singletons.TypeLits Methods compare :: Nat -> Nat -> Ordering # (<) :: Nat -> Nat -> Bool # (<=) :: Nat -> Nat -> Bool # (>) :: Nat -> Nat -> Bool # (>=) :: Nat -> Nat -> Bool # max :: Nat -> Nat -> Nat # min :: Nat -> Nat -> Nat #
Show Nat Source #
Instance details Defined in Data.Singletons.TypeLits Methods showsPrec :: Int -> Nat -> ShowS # show :: Nat -> String # showList :: [Nat] -> ShowS #
SingKind Nat Source #
Instance details Defined in Data.Singletons.TypeLits.Internal Associated Types type Demote Nat = (r :: Type) Source # Methods fromSing :: forall (a :: Nat). Sing a -> Demote Nat Source # toSing :: Demote Nat -> SomeSing Nat Source #
SDecide Nat Source #
Instance details Defined in Data.Singletons.TypeLits.Internal Methods (%~) :: forall (a :: Nat) (b :: Nat). Sing a -> Sing b -> Decision (a :~: b) Source #
PEq Nat Source #
Instance details Defined in Data.Singletons.TypeLits.Internal Associated Types type x == y :: Bool Source # type x /= y :: Bool Source #
SEq Nat Source #
Instance details Defined in Data.Singletons.TypeLits.Internal Methods (%==) :: forall (a :: Nat) (b :: Nat). Sing a -> Sing b -> Sing (a == b) Source # (%/=) :: forall (a :: Nat) (b :: Nat). Sing a -> Sing b -> Sing (a /= b) Source #
SOrd Nat Source #
Instance details Defined in Data.Singletons.TypeLits.Internal Methods sCompare :: forall (t :: Nat) (t :: Nat). Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source # (%<) :: forall (t :: Nat) (t :: Nat). Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source # (%<=) :: forall (t :: Nat) (t :: Nat). Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source # (%>) :: forall (t :: Nat) (t :: Nat). Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source # (%>=) :: forall (t :: Nat) (t :: Nat). Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source # sMax :: forall (t :: Nat) (t :: Nat). Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source # sMin :: forall (t :: Nat) (t :: Nat). Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source #
POrd Nat Source #
Instance details Defined in Data.Singletons.TypeLits.Internal Associated Types type Compare arg arg :: Ordering Source # type arg < arg :: Bool Source # type arg <= arg :: Bool Source # type arg > arg :: Bool Source # type arg >= arg :: Bool Source # type Max arg arg :: a Source # type Min arg arg :: a Source #
SNum Nat Source #
Instance details Defined in Data.Singletons.Prelude.Num Methods (%+) :: forall (t :: Nat) (t :: Nat). Sing t -> Sing t -> Sing (Apply (Apply (+@#@$) t) t) Source # (%-) :: forall (t :: Nat) (t :: Nat). Sing t -> Sing t -> Sing (Apply (Apply (-@#@$) t) t) Source # (%) :: forall (t :: Nat) (t :: Nat). Sing t -> Sing t -> Sing (Apply (Apply (@#@$) t) t) Source # sNegate :: forall (t :: Nat). Sing t -> Sing (Apply NegateSym0 t) Source # sAbs :: forall (t :: Nat). Sing t -> Sing (Apply AbsSym0 t) Source # sSignum :: forall (t :: Nat). Sing t -> Sing (Apply SignumSym0 t) Source # sFromInteger :: forall (t :: Nat). Sing t -> Sing (Apply FromIntegerSym0 t) Source #
PNum Nat Source #
Instance details Defined in Data.Singletons.Prelude.Num Associated Types type arg + arg :: a Source # type arg - arg :: a Source # type arg * arg :: a Source # type Negate arg :: a Source # type Abs arg :: a Source # type Signum arg :: a Source # type FromInteger arg :: a Source #
SEnum Nat Source #
Instance details Defined in Data.Singletons.Prelude.Enum Methods sSucc :: forall (t :: Nat). Sing t -> Sing (Apply SuccSym0 t) Source # sPred :: forall (t :: Nat). Sing t -> Sing (Apply PredSym0 t) Source # sToEnum :: forall (t :: Nat). Sing t -> Sing (Apply ToEnumSym0 t) Source # sFromEnum :: forall (t :: Nat). Sing t -> Sing (Apply FromEnumSym0 t) Source # sEnumFromTo :: forall (t :: Nat) (t :: Nat). Sing t -> Sing t -> Sing (Apply (Apply EnumFromToSym0 t) t) Source # sEnumFromThenTo :: forall (t :: Nat) (t :: Nat) (t :: Nat). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply EnumFromThenToSym0 t) t) t) Source #
PEnum Nat Source #
Instance details Defined in Data.Singletons.Prelude.Enum Associated Types type Succ arg :: a Source # type Pred arg :: a Source # type ToEnum arg :: a Source # type FromEnum arg :: Nat Source # type EnumFromTo arg arg :: [a] Source # type EnumFromThenTo arg arg arg :: [a] Source #
SShow Nat Source #
Instance details Defined in Data.Singletons.Prelude.Show Methods sShowsPrec :: forall (t :: Nat) (t :: Nat) (t :: Symbol). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply ShowsPrecSym0 t) t) t) Source # sShow_ :: forall (t :: Nat). Sing t -> Sing (Apply Show_Sym0 t) Source # sShowList :: forall (t :: [Nat]) (t :: Symbol). Sing t -> Sing t -> Sing (Apply (Apply ShowListSym0 t) t) Source #
PShow Nat Source #
Instance details Defined in Data.Singletons.Prelude.Show Associated Types type ShowsPrec arg arg arg :: Symbol Source # type Show_ arg :: Symbol Source # type ShowList arg arg :: Symbol Source #
KnownNat n => SingI (n :: Nat) Source #
Instance details Defined in Data.Singletons.TypeLits.Internal Methods sing :: Sing n Source #
SingI Log2Sym0 Source #
Instance details Defined in Data.Singletons.TypeLits Methods sing :: Sing Log2Sym0 Source #
SingI (<=?@#@$) Source #
Instance details Defined in Data.Singletons.TypeLits.Internal Methods sing :: Sing (<=?@#@$) Source #
SingI (^@#@$) Source #
Instance details Defined in Data.Singletons.TypeLits.Internal Methods sing :: Sing (^@#@$) Source #
SingI DivSym0 Source #
Instance details Defined in Data.Singletons.TypeLits Methods sing :: Sing DivSym0 Source #
SingI ModSym0 Source #
Instance details Defined in Data.Singletons.TypeLits Methods sing :: Sing ModSym0 Source #
SuppressUnusedWarnings KnownNatSym0 Source #
Instance details Defined in Data.Singletons.TypeLits Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings Log2Sym0 Source #
Instance details Defined in Data.Singletons.TypeLits Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (<=?@#@$) Source #
Instance details Defined in Data.Singletons.TypeLits.Internal Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (^@#@$) Source #
Instance details Defined in Data.Singletons.TypeLits.Internal Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings DivSym0 Source #
Instance details Defined in Data.Singletons.TypeLits Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings ModSym0 Source #
Instance details Defined in Data.Singletons.TypeLits Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings QuotSym0 Source #
Instance details Defined in Data.Singletons.TypeLits Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings RemSym0 Source #
Instance details Defined in Data.Singletons.TypeLits Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings DivModSym0 Source #
Instance details Defined in Data.Singletons.TypeLits Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings QuotRemSym0 Source #
Instance details Defined in Data.Singletons.TypeLits Methods suppressUnusedWarnings :: () Source #
SingI x => SingI ((<=?@#@$$) x :: TyFun Nat Bool -> Type) Source #
Instance details Defined in Data.Singletons.TypeLits.Internal Methods sing :: Sing ((<=?@#@$$) x) Source #
SingI x => SingI ((^@#@$$) x :: TyFun Nat Nat -> Type) Source #
Instance details Defined in Data.Singletons.TypeLits.Internal Methods sing :: Sing ((^@#@$$) x) Source #
SingI x => SingI (DivSym1 x :: TyFun Nat Nat -> Type) Source #
Instance details Defined in Data.Singletons.TypeLits Methods sing :: Sing (DivSym1 x) Source #
SingI x => SingI (ModSym1 x :: TyFun Nat Nat -> Type) Source #
Instance details Defined in Data.Singletons.TypeLits Methods sing :: Sing (ModSym1 x) Source #
SingI ((!!@#@$) :: TyFun [a] (Nat ~> a) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (!!@#@$) Source #
SNum a => SingI (FromIntegerSym0 :: TyFun Nat a -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Num Methods sing :: Sing FromIntegerSym0 Source #
SEnum a => SingI (ToEnumSym0 :: TyFun Nat a -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Enum Methods sing :: Sing ToEnumSym0 Source #
SingI (SplitAtSym0 :: TyFun Nat ([a] ~> ([a], [a])) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing SplitAtSym0 Source #
SingI (DropSym0 :: TyFun Nat ([a] ~> [a]) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing DropSym0 Source #
SingI (TakeSym0 :: TyFun Nat ([a] ~> [a]) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing TakeSym0 Source #
SingI (ReplicateSym0 :: TyFun Nat (a ~> [a]) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing ReplicateSym0 Source #
SShow a => SingI (ShowsPrecSym0 :: TyFun Nat (a ~> (Symbol ~> Symbol)) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Show Methods sing :: Sing ShowsPrecSym0 Source #
SingI (SplitAtSym0 :: TyFun Nat (NonEmpty a ~> ([a], [a])) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods sing :: Sing SplitAtSym0 Source #
SingI (DropSym0 :: TyFun Nat (NonEmpty a ~> [a]) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods sing :: Sing DropSym0 Source #
SingI (TakeSym0 :: TyFun Nat (NonEmpty a ~> [a]) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods sing :: Sing TakeSym0 Source #
SEnum a => SingI (FromEnumSym0 :: TyFun a Nat -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Enum Methods sing :: Sing FromEnumSym0 Source #
SEq a => SingI (ElemIndicesSym0 :: TyFun a ([a] ~> [Nat]) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing ElemIndicesSym0 Source #
SEq a => SingI (ElemIndexSym0 :: TyFun a ([a] ~> Maybe Nat) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing ElemIndexSym0 Source #
SingI ((!!@#@$) :: TyFun (NonEmpty a) (Nat ~> a) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods sing :: Sing (!!@#@$) Source #
SingI (LengthSym0 :: TyFun (NonEmpty a) Nat -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods sing :: Sing LengthSym0 Source #
SingI (FindIndicesSym0 :: TyFun (a ~> Bool) ([a] ~> [Nat]) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing FindIndicesSym0 Source #
SingI (FindIndexSym0 :: TyFun (a ~> Bool) ([a] ~> Maybe Nat) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing FindIndexSym0 Source #
SuppressUnusedWarnings ((!!@#@$) :: TyFun [a] (Nat ~> a) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings ((<=?@#@$$) a6989586621679473158 :: TyFun Nat Bool -> Type) Source #
Instance details Defined in Data.Singletons.TypeLits.Internal Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings ((^@#@$$) a6989586621679472866 :: TyFun Nat Nat -> Type) Source #
Instance details Defined in Data.Singletons.TypeLits.Internal Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (DivSym1 a6989586621679492680 :: TyFun Nat Nat -> Type) Source #
Instance details Defined in Data.Singletons.TypeLits Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (ModSym1 a6989586621679493016 :: TyFun Nat Nat -> Type) Source #
Instance details Defined in Data.Singletons.TypeLits Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (QuotSym1 a6989586621679493492 :: TyFun Nat Nat -> Type) Source #
Instance details Defined in Data.Singletons.TypeLits Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (RemSym1 a6989586621679493481 :: TyFun Nat Nat -> Type) Source #
Instance details Defined in Data.Singletons.TypeLits Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (DivModSym1 a6989586621679493510 :: TyFun Nat (Nat, Nat) -> Type) Source #
Instance details Defined in Data.Singletons.TypeLits Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (QuotRemSym1 a6989586621679493503 :: TyFun Nat (Nat, Nat) -> Type) Source #
Instance details Defined in Data.Singletons.TypeLits Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (FromIntegerSym0 :: TyFun Nat a -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Num Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (ToEnumSym0 :: TyFun Nat a -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Enum Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (DropSym0 :: TyFun Nat ([a] ~> [a]) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (TakeSym0 :: TyFun Nat ([a] ~> [a]) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (SplitAtSym0 :: TyFun Nat ([a] ~> ([a], [a])) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (ReplicateSym0 :: TyFun Nat (a ~> [a]) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (ShowsPrecSym0 :: TyFun Nat (a ~> (Symbol ~> Symbol)) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Show Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (TakeSym0 :: TyFun Nat (NonEmpty a ~> [a]) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (DropSym0 :: TyFun Nat (NonEmpty a ~> [a]) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (SplitAtSym0 :: TyFun Nat (NonEmpty a ~> ([a], [a])) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (FromEnumSym0 :: TyFun a Nat -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Enum Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (ElemIndicesSym0 :: TyFun a ([a] ~> [Nat]) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (ElemIndexSym0 :: TyFun a ([a] ~> Maybe Nat) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings ((!!@#@$) :: TyFun (NonEmpty a) (Nat ~> a) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (LengthSym0 :: TyFun (NonEmpty a) Nat -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (FindIndicesSym0 :: TyFun (a ~> Bool) ([a] ~> [Nat]) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (FindIndexSym0 :: TyFun (a ~> Bool) ([a] ~> Maybe Nat) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods suppressUnusedWarnings :: () Source #
SingI d => SingI (FindIndicesSym1 d :: TyFun [a] [Nat] -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (FindIndicesSym1 d) Source #
SingI d => SingI (FindIndexSym1 d :: TyFun [a] (Maybe Nat) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (FindIndexSym1 d) Source #
(SEq a, SingI d) => SingI (ElemIndicesSym1 d :: TyFun [a] [Nat] -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (ElemIndicesSym1 d) Source #
(SEq a, SingI d) => SingI (ElemIndexSym1 d :: TyFun [a] (Maybe Nat) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (ElemIndexSym1 d) Source #
SingI d => SingI ((!!@#@$$) d :: TyFun Nat a -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing ((!!@#@$$) d) Source #
SingI d => SingI ((!!@#@$$) d :: TyFun Nat a -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods sing :: Sing ((!!@#@$$) d) Source #
SApplicative m => SingI (ReplicateM_Sym0 :: TyFun Nat (m a ~> m ()) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Monad Methods sing :: Sing ReplicateM_Sym0 Source #
SApplicative m => SingI (ReplicateMSym0 :: TyFun Nat (m a ~> m [a]) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Monad Methods sing :: Sing ReplicateMSym0 Source #
SuppressUnusedWarnings (FindIndicesSym1 a6989586621679969210 :: TyFun [a] [Nat] -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (ElemIndicesSym1 a6989586621679969242 :: TyFun [a] [Nat] -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (FindIndexSym1 a6989586621679969233 :: TyFun [a] (Maybe Nat) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (ElemIndexSym1 a6989586621679969251 :: TyFun [a] (Maybe Nat) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings ((!!@#@$$) a6989586621679968875 :: TyFun Nat a -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings ((!!@#@$$) a6989586621681185857 :: TyFun Nat a -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (ReplicateM_Sym0 :: TyFun Nat (m a ~> m ()) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Monad Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (ReplicateMSym0 :: TyFun Nat (m a ~> m [a]) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Monad Methods suppressUnusedWarnings :: () Source #
SFoldable t => SingI (LengthSym0 :: TyFun (t a) Nat -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing LengthSym0 Source #
SuppressUnusedWarnings (LengthSym0 :: TyFun (t a) Nat -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Foldable Methods suppressUnusedWarnings :: () Source #
type Demote Nat Source #
Instance details Defined in Data.Singletons.TypeLits.Internal type Demote Nat = Natural
type Sing Source #
Instance details Defined in Data.Singletons.TypeLits.Internal type Sing = SNat
type Negate (a :: Nat) Source #
Instance details Defined in Data.Singletons.Prelude.Num type Negate (a :: Nat) = Error "Cannot negate a natural number" :: Nat
type Abs (a :: Nat) Source #
Instance details Defined in Data.Singletons.Prelude.Num type Abs (a :: Nat) = a
type Signum (a :: Nat) Source #
Instance details Defined in Data.Singletons.Prelude.Num type Signum (a :: Nat)
type FromInteger a Source #
Instance details Defined in Data.Singletons.Prelude.Num type FromInteger a = a
type Succ (a :: Nat) Source #
Instance details Defined in Data.Singletons.Prelude.Enum type Succ (a :: Nat)
type Pred (a :: Nat) Source #
Instance details Defined in Data.Singletons.Prelude.Enum type Pred (a :: Nat)
type ToEnum a Source #
Instance details Defined in Data.Singletons.Prelude.Enum type ToEnum a
type FromEnum (a :: Nat) Source #
Instance details Defined in Data.Singletons.Prelude.Enum type FromEnum (a :: Nat)
type Show_ (arg :: Nat) Source #
Instance details Defined in Data.Singletons.Prelude.Show type Show_ (arg :: Nat)
type (x :: Nat) == (y :: Nat) Source #
Instance details Defined in Data.Singletons.TypeLits.Internal type (x :: Nat) == (y :: Nat) = DefaultEq x y
type (x :: Nat) /= (y :: Nat) Source #
Instance details Defined in Data.Singletons.TypeLits.Internal type (x :: Nat) /= (y :: Nat) = Not (x == y)
type Compare (a :: Nat) (b :: Nat) Source #
Instance details Defined in Data.Singletons.TypeLits.Internal type Compare (a :: Nat) (b :: Nat) = CmpNat a b
type (arg1 :: Nat) < (arg2 :: Nat) Source #
Instance details Defined in Data.Singletons.TypeLits.Internal type (arg1 :: Nat) < (arg2 :: Nat)
type (arg1 :: Nat) <= (arg2 :: Nat) Source #
Instance details Defined in Data.Singletons.TypeLits.Internal type (arg1 :: Nat) <= (arg2 :: Nat)
type (arg1 :: Nat) > (arg2 :: Nat) Source #
Instance details Defined in Data.Singletons.TypeLits.Internal type (arg1 :: Nat) > (arg2 :: Nat)
type (arg1 :: Nat) >= (arg2 :: Nat) Source #
Instance details Defined in Data.Singletons.TypeLits.Internal type (arg1 :: Nat) >= (arg2 :: Nat)
type Max (arg1 :: Nat) (arg2 :: Nat) Source #
Instance details Defined in Data.Singletons.TypeLits.Internal type Max (arg1 :: Nat) (arg2 :: Nat)
type Min (arg1 :: Nat) (arg2 :: Nat) Source #
Instance details Defined in Data.Singletons.TypeLits.Internal type Min (arg1 :: Nat) (arg2 :: Nat)
type (a :: Nat) + (b :: Nat) Source #
Instance details Defined in Data.Singletons.Prelude.Num type (a :: Nat) + (b :: Nat) = a + b
type (a :: Nat) - (b :: Nat) Source #
Instance details Defined in Data.Singletons.Prelude.Num type (a :: Nat) - (b :: Nat) = a - b
type (a :: Nat) * (b :: Nat) Source #
Instance details Defined in Data.Singletons.Prelude.Num type (a :: Nat) * (b :: Nat) = a * b
type EnumFromTo (a1 :: Nat) (a2 :: Nat) Source #
Instance details Defined in Data.Singletons.Prelude.Enum type EnumFromTo (a1 :: Nat) (a2 :: Nat)
type ShowList (arg1 :: [Nat]) arg2 Source #
Instance details Defined in Data.Singletons.Prelude.Show type ShowList (arg1 :: [Nat]) arg2
type Apply KnownNatSym0 (a6989586621679491988 :: Nat) Source #
Instance details Defined in Data.Singletons.TypeLits type Apply KnownNatSym0 (a6989586621679491988 :: Nat) = KnownNatSym1 a6989586621679491988
type Apply Log2Sym0 (a6989586621679492472 :: Nat) Source #
Instance details Defined in Data.Singletons.TypeLits type Apply Log2Sym0 (a6989586621679492472 :: Nat) = Log2Sym1 a6989586621679492472
type EnumFromThenTo (a1 :: Nat) (a2 :: Nat) (a3 :: Nat) Source #
Instance details Defined in Data.Singletons.Prelude.Enum type EnumFromThenTo (a1 :: Nat) (a2 :: Nat) (a3 :: Nat)
type ShowsPrec _1 (n :: Nat) x Source #
Instance details Defined in Data.Singletons.Prelude.Show type ShowsPrec _1 (n :: Nat) x
type Apply ((<=?@#@$$) a6989586621679473158 :: TyFun Nat Bool -> Type) (a6989586621679473159 :: Nat) Source #
Instance details Defined in Data.Singletons.TypeLits.Internal type Apply ((<=?@#@$$) a6989586621679473158 :: TyFun Nat Bool -> Type) (a6989586621679473159 :: Nat) = a6989586621679473158 <=?@#@$$$ a6989586621679473159
type Apply ((^@#@$$) a6989586621679472866 :: TyFun Nat Nat -> Type) (a6989586621679472867 :: Nat) Source #
Instance details Defined in Data.Singletons.TypeLits.Internal type Apply ((^@#@$$) a6989586621679472866 :: TyFun Nat Nat -> Type) (a6989586621679472867 :: Nat) = a6989586621679472866 ^@#@$$$ a6989586621679472867
type Apply (DivSym1 a6989586621679492680 :: TyFun Nat Nat -> Type) (a6989586621679492681 :: Nat) Source #
Instance details Defined in Data.Singletons.TypeLits type Apply (DivSym1 a6989586621679492680 :: TyFun Nat Nat -> Type) (a6989586621679492681 :: Nat) = DivSym2 a6989586621679492680 a6989586621679492681
type Apply (ModSym1 a6989586621679493016 :: TyFun Nat Nat -> Type) (a6989586621679493017 :: Nat) Source #
Instance details Defined in Data.Singletons.TypeLits type Apply (ModSym1 a6989586621679493016 :: TyFun Nat Nat -> Type) (a6989586621679493017 :: Nat) = ModSym2 a6989586621679493016 a6989586621679493017
type Apply (QuotSym1 a6989586621679493492 :: TyFun Nat Nat -> Type) (a6989586621679493493 :: Nat) Source #
Instance details Defined in Data.Singletons.TypeLits type Apply (QuotSym1 a6989586621679493492 :: TyFun Nat Nat -> Type) (a6989586621679493493 :: Nat) = QuotSym2 a6989586621679493492 a6989586621679493493
type Apply (RemSym1 a6989586621679493481 :: TyFun Nat Nat -> Type) (a6989586621679493482 :: Nat) Source #
Instance details Defined in Data.Singletons.TypeLits type Apply (RemSym1 a6989586621679493481 :: TyFun Nat Nat -> Type) (a6989586621679493482 :: Nat) = RemSym2 a6989586621679493481 a6989586621679493482
type Apply (FromIntegerSym0 :: TyFun Nat k2 -> Type) (a6989586621679517819 :: Nat) Source #
Instance details Defined in Data.Singletons.Prelude.Num type Apply (FromIntegerSym0 :: TyFun Nat k2 -> Type) (a6989586621679517819 :: Nat) = FromIntegerSym1 a6989586621679517819 :: k2
type Apply (ToEnumSym0 :: TyFun Nat k2 -> Type) (a6989586621679758475 :: Nat) Source #
Instance details Defined in Data.Singletons.Prelude.Enum type Apply (ToEnumSym0 :: TyFun Nat k2 -> Type) (a6989586621679758475 :: Nat) = ToEnumSym1 a6989586621679758475 :: k2
type Apply (FromEnumSym0 :: TyFun a Nat -> Type) (a6989586621679758478 :: a) Source #
Instance details Defined in Data.Singletons.Prelude.Enum type Apply (FromEnumSym0 :: TyFun a Nat -> Type) (a6989586621679758478 :: a) = FromEnumSym1 a6989586621679758478
type Apply ((!!@#@$$) a6989586621679968875 :: TyFun Nat a -> Type) (a6989586621679968876 :: Nat) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal type Apply ((!!@#@$$) a6989586621679968875 :: TyFun Nat a -> Type) (a6989586621679968876 :: Nat) = a6989586621679968875 !!@#@$$$ a6989586621679968876
type Apply ((!!@#@$$) a6989586621681185857 :: TyFun Nat a -> Type) (a6989586621681185858 :: Nat) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty type Apply ((!!@#@$$) a6989586621681185857 :: TyFun Nat a -> Type) (a6989586621681185858 :: Nat) = a6989586621681185857 !!@#@$$$ a6989586621681185858
type Apply (<=?@#@$) (a6989586621679473158 :: Nat) Source #
Instance details Defined in Data.Singletons.TypeLits.Internal type Apply (<=?@#@$) (a6989586621679473158 :: Nat) = (<=?@#@$$) a6989586621679473158
type Apply (^@#@$) (a6989586621679472866 :: Nat) Source #
Instance details Defined in Data.Singletons.TypeLits.Internal type Apply (^@#@$) (a6989586621679472866 :: Nat) = (^@#@$$) a6989586621679472866
type Apply DivSym0 (a6989586621679492680 :: Nat) Source #
Instance details Defined in Data.Singletons.TypeLits type Apply DivSym0 (a6989586621679492680 :: Nat) = DivSym1 a6989586621679492680
type Apply ModSym0 (a6989586621679493016 :: Nat) Source #
Instance details Defined in Data.Singletons.TypeLits type Apply ModSym0 (a6989586621679493016 :: Nat) = ModSym1 a6989586621679493016
type Apply QuotSym0 (a6989586621679493492 :: Nat) Source #
Instance details Defined in Data.Singletons.TypeLits type Apply QuotSym0 (a6989586621679493492 :: Nat) = QuotSym1 a6989586621679493492
type Apply RemSym0 (a6989586621679493481 :: Nat) Source #
Instance details Defined in Data.Singletons.TypeLits type Apply RemSym0 (a6989586621679493481 :: Nat) = RemSym1 a6989586621679493481
type Apply DivModSym0 (a6989586621679493510 :: Nat) Source #
Instance details Defined in Data.Singletons.TypeLits type Apply DivModSym0 (a6989586621679493510 :: Nat) = DivModSym1 a6989586621679493510
type Apply QuotRemSym0 (a6989586621679493503 :: Nat) Source #
Instance details Defined in Data.Singletons.TypeLits type Apply QuotRemSym0 (a6989586621679493503 :: Nat) = QuotRemSym1 a6989586621679493503
type Apply (DivModSym1 a6989586621679493510 :: TyFun Nat (Nat, Nat) -> Type) (a6989586621679493511 :: Nat) Source #
Instance details Defined in Data.Singletons.TypeLits type Apply (DivModSym1 a6989586621679493510 :: TyFun Nat (Nat, Nat) -> Type) (a6989586621679493511 :: Nat) = DivModSym2 a6989586621679493510 a6989586621679493511
type Apply (QuotRemSym1 a6989586621679493503 :: TyFun Nat (Nat, Nat) -> Type) (a6989586621679493504 :: Nat) Source #
Instance details Defined in Data.Singletons.TypeLits type Apply (QuotRemSym1 a6989586621679493503 :: TyFun Nat (Nat, Nat) -> Type) (a6989586621679493504 :: Nat) = QuotRemSym2 a6989586621679493503 a6989586621679493504
type Apply (DropSym0 :: TyFun Nat ([a] ~> [a]) -> Type) (a6989586621679969037 :: Nat) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal type Apply (DropSym0 :: TyFun Nat ([a] ~> [a]) -> Type) (a6989586621679969037 :: Nat) = DropSym1 a6989586621679969037 :: TyFun [a] [a] -> Type
type Apply (TakeSym0 :: TyFun Nat ([a] ~> [a]) -> Type) (a6989586621679969050 :: Nat) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal type Apply (TakeSym0 :: TyFun Nat ([a] ~> [a]) -> Type) (a6989586621679969050 :: Nat) = TakeSym1 a6989586621679969050 :: TyFun [a] [a] -> Type
type Apply (SplitAtSym0 :: TyFun Nat ([a] ~> ([a], [a])) -> Type) (a6989586621679969030 :: Nat) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal type Apply (SplitAtSym0 :: TyFun Nat ([a] ~> ([a], [a])) -> Type) (a6989586621679969030 :: Nat) = SplitAtSym1 a6989586621679969030 :: TyFun [a] ([a], [a]) -> Type
type Apply (ReplicateSym0 :: TyFun Nat (a ~> [a]) -> Type) (a6989586621679968895 :: Nat) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal type Apply (ReplicateSym0 :: TyFun Nat (a ~> [a]) -> Type) (a6989586621679968895 :: Nat) = ReplicateSym1 a6989586621679968895 :: TyFun a [a] -> Type
type Apply (ShowsPrecSym0 :: TyFun Nat (a ~> (Symbol ~> Symbol)) -> Type) (a6989586621680279568 :: Nat) Source #
Instance details Defined in Data.Singletons.Prelude.Show type Apply (ShowsPrecSym0 :: TyFun Nat (a ~> (Symbol ~> Symbol)) -> Type) (a6989586621680279568 :: Nat) = ShowsPrecSym1 a6989586621680279568 :: TyFun a (Symbol ~> Symbol) -> Type
type Apply (TakeSym0 :: TyFun Nat (NonEmpty a ~> [a]) -> Type) (a6989586621681186067 :: Nat) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty type Apply (TakeSym0 :: TyFun Nat (NonEmpty a ~> [a]) -> Type) (a6989586621681186067 :: Nat) = TakeSym1 a6989586621681186067 :: TyFun (NonEmpty a) [a] -> Type
type Apply (DropSym0 :: TyFun Nat (NonEmpty a ~> [a]) -> Type) (a6989586621681186058 :: Nat) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty type Apply (DropSym0 :: TyFun Nat (NonEmpty a ~> [a]) -> Type) (a6989586621681186058 :: Nat) = DropSym1 a6989586621681186058 :: TyFun (NonEmpty a) [a] -> Type
type Apply (SplitAtSym0 :: TyFun Nat (NonEmpty a ~> ([a], [a])) -> Type) (a6989586621681186049 :: Nat) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty type Apply (SplitAtSym0 :: TyFun Nat (NonEmpty a ~> ([a], [a])) -> Type) (a6989586621681186049 :: Nat) = SplitAtSym1 a6989586621681186049 :: TyFun (NonEmpty a) ([a], [a]) -> Type
type Apply (ElemIndicesSym0 :: TyFun a ([a] ~> [Nat]) -> Type) (a6989586621679969242 :: a) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal type Apply (ElemIndicesSym0 :: TyFun a ([a] ~> [Nat]) -> Type) (a6989586621679969242 :: a) = ElemIndicesSym1 a6989586621679969242
type Apply (ElemIndexSym0 :: TyFun a ([a] ~> Maybe Nat) -> Type) (a6989586621679969251 :: a) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal type Apply (ElemIndexSym0 :: TyFun a ([a] ~> Maybe Nat) -> Type) (a6989586621679969251 :: a) = ElemIndexSym1 a6989586621679969251
type Apply (ReplicateM_Sym0 :: TyFun Nat (m a ~> m ()) -> Type) (a6989586621681292275 :: Nat) Source #
Instance details Defined in Data.Singletons.Prelude.Monad type Apply (ReplicateM_Sym0 :: TyFun Nat (m a ~> m ()) -> Type) (a6989586621681292275 :: Nat) = ReplicateM_Sym1 a6989586621681292275 :: TyFun (m a) (m ()) -> Type
type Apply (ReplicateMSym0 :: TyFun Nat (m a ~> m [a]) -> Type) (a6989586621681292293 :: Nat) Source #
Instance details Defined in Data.Singletons.Prelude.Monad type Apply (ReplicateMSym0 :: TyFun Nat (m a ~> m [a]) -> Type) (a6989586621681292293 :: Nat) = ReplicateMSym1 a6989586621681292293 :: TyFun (m a) (m [a]) -> Type
type Apply (LengthSym0 :: TyFun (NonEmpty a) Nat -> Type) (a6989586621681186282 :: NonEmpty a) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty type Apply (LengthSym0 :: TyFun (NonEmpty a) Nat -> Type) (a6989586621681186282 :: NonEmpty a) = LengthSym1 a6989586621681186282
type Apply (LengthSym0 :: TyFun (t a) Nat -> Type) (a6989586621680492493 :: t a) Source #
Instance details Defined in Data.Singletons.Prelude.Foldable type Apply (LengthSym0 :: TyFun (t a) Nat -> Type) (a6989586621680492493 :: t a) = LengthSym1 a6989586621680492493
type Apply (FindIndicesSym1 a6989586621679969210 :: TyFun [a] [Nat] -> Type) (a6989586621679969211 :: [a]) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal type Apply (FindIndicesSym1 a6989586621679969210 :: TyFun [a] [Nat] -> Type) (a6989586621679969211 :: [a]) = FindIndicesSym2 a6989586621679969210 a6989586621679969211
type Apply (ElemIndicesSym1 a6989586621679969242 :: TyFun [a] [Nat] -> Type) (a6989586621679969243 :: [a]) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal type Apply (ElemIndicesSym1 a6989586621679969242 :: TyFun [a] [Nat] -> Type) (a6989586621679969243 :: [a]) = ElemIndicesSym2 a6989586621679969242 a6989586621679969243
type Apply (FindIndexSym1 a6989586621679969233 :: TyFun [a] (Maybe Nat) -> Type) (a6989586621679969234 :: [a]) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal type Apply (FindIndexSym1 a6989586621679969233 :: TyFun [a] (Maybe Nat) -> Type) (a6989586621679969234 :: [a]) = FindIndexSym2 a6989586621679969233 a6989586621679969234
type Apply (ElemIndexSym1 a6989586621679969251 :: TyFun [a] (Maybe Nat) -> Type) (a6989586621679969252 :: [a]) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal type Apply (ElemIndexSym1 a6989586621679969251 :: TyFun [a] (Maybe Nat) -> Type) (a6989586621679969252 :: [a]) = ElemIndexSym2 a6989586621679969251 a6989586621679969252
type Apply ((!!@#@$) :: TyFun [a] (Nat ~> a) -> Type) (a6989586621679968875 :: [a]) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal type Apply ((!!@#@$) :: TyFun [a] (Nat ~> a) -> Type) (a6989586621679968875 :: [a]) = (!!@#@$$) a6989586621679968875
type Apply ((!!@#@$) :: TyFun (NonEmpty a) (Nat ~> a) -> Type) (a6989586621681185857 :: NonEmpty a) Source #
Instance details Defined in Data.Singletons.Prelude.List.NonEmpty type Apply ((!!@#@$) :: TyFun (NonEmpty a) (Nat ~> a) -> Type) (a6989586621681185857 :: NonEmpty a) = (!!@#@$$) a6989586621681185857
type Apply (FindIndicesSym0 :: TyFun (a ~> Bool) ([a] ~> [Nat]) -> Type) (a6989586621679969210 :: a ~> Bool) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal type Apply (FindIndicesSym0 :: TyFun (a ~> Bool) ([a] ~> [Nat]) -> Type) (a6989586621679969210 :: a ~> Bool) = FindIndicesSym1 a6989586621679969210
type Apply (FindIndexSym0 :: TyFun (a ~> Bool) ([a] ~> Maybe Nat) -> Type) (a6989586621679969233 :: a ~> Bool) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal type Apply (FindIndexSym0 :: TyFun (a ~> Bool) ([a] ~> Maybe Nat) -> Type) (a6989586621679969233 :: a ~> Bool) = FindIndexSym1 a6989586621679969233

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 Data.Singletons.TypeLits Methods (==) :: Symbol -> Symbol -> Bool # (/=) :: Symbol -> Symbol -> Bool #
Ord Symbol Source #
Instance details Defined in Data.Singletons.TypeLits Methods compare :: Symbol -> Symbol -> Ordering # (<) :: Symbol -> Symbol -> Bool # (<=) :: Symbol -> Symbol -> Bool # (>) :: Symbol -> Symbol -> Bool # (>=) :: Symbol -> Symbol -> Bool # max :: Symbol -> Symbol -> Symbol # min :: Symbol -> Symbol -> Symbol #
Show Symbol Source #
Instance details Defined in Data.Singletons.TypeLits Methods showsPrec :: Int -> Symbol -> ShowS # show :: Symbol -> String # showList :: [Symbol] -> ShowS #
IsString Symbol Source #
Instance details Defined in Data.Singletons.TypeLits Methods fromString :: String -> Symbol #
Semigroup Symbol Source #
Instance details Defined in Data.Singletons.TypeLits Methods (<>) :: Symbol -> Symbol -> Symbol # sconcat :: NonEmpty Symbol -> Symbol # stimes :: Integral b => b -> Symbol -> Symbol #
Monoid Symbol Source #
Instance details Defined in Data.Singletons.TypeLits Methods mempty :: Symbol # mappend :: Symbol -> Symbol -> Symbol # mconcat :: [Symbol] -> Symbol #
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
SingKind Symbol Source #
Instance details Defined in Data.Singletons.TypeLits.Internal Associated Types type Demote Symbol = (r :: Type) Source # Methods fromSing :: forall (a :: Symbol). Sing a -> Demote Symbol Source # toSing :: Demote Symbol -> SomeSing Symbol Source #
SingKind PErrorMessage Source #
Instance details Defined in Data.Singletons.TypeError Associated Types type Demote PErrorMessage = (r :: Type) Source # Methods fromSing :: forall (a :: PErrorMessage). Sing a -> Demote PErrorMessage Source # toSing :: Demote PErrorMessage -> SomeSing PErrorMessage Source #
SDecide Symbol Source #
Instance details Defined in Data.Singletons.TypeLits.Internal Methods (%~) :: forall (a :: Symbol) (b :: Symbol). Sing a -> Sing b -> Decision (a :~: b) Source #
PEq Symbol Source #
Instance details Defined in Data.Singletons.TypeLits.Internal Associated Types type x == y :: Bool Source # type x /= y :: Bool Source #
SEq Symbol Source #
Instance details Defined in Data.Singletons.TypeLits.Internal Methods (%==) :: forall (a :: Symbol) (b :: Symbol). Sing a -> Sing b -> Sing (a == b) Source # (%/=) :: forall (a :: Symbol) (b :: Symbol). Sing a -> Sing b -> Sing (a /= b) Source #
SOrd Symbol Source #
Instance details Defined in Data.Singletons.TypeLits.Internal Methods sCompare :: forall (t :: Symbol) (t :: Symbol). Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source # (%<) :: forall (t :: Symbol) (t :: Symbol). Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source # (%<=) :: forall (t :: Symbol) (t :: Symbol). Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source # (%>) :: forall (t :: Symbol) (t :: Symbol). Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source # (%>=) :: forall (t :: Symbol) (t :: Symbol). Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source # sMax :: forall (t :: Symbol) (t :: Symbol). Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source # sMin :: forall (t :: Symbol) (t :: Symbol). Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source #
POrd Symbol Source #
Instance details Defined in Data.Singletons.TypeLits.Internal Associated Types type Compare arg arg :: Ordering Source # type arg < arg :: Bool Source # type arg <= arg :: Bool Source # type arg > arg :: Bool Source # type arg >= arg :: Bool Source # type Max arg arg :: a Source # type Min arg arg :: a Source #
SSemigroup Symbol Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Methods (%<>) :: forall (t :: Symbol) (t :: Symbol). Sing t -> Sing t -> Sing (Apply (Apply (<>@#@$) t) t) Source # sSconcat :: forall (t :: NonEmpty Symbol). Sing t -> Sing (Apply SconcatSym0 t) Source #
PSemigroup Symbol Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Associated Types type arg <> arg :: a Source # type Sconcat arg :: a Source #
SShow Symbol Source #
Instance details Defined in Data.Singletons.Prelude.Show Methods sShowsPrec :: forall (t :: Nat) (t :: Symbol) (t :: Symbol). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply ShowsPrecSym0 t) t) t) Source # sShow_ :: forall (t :: Symbol). Sing t -> Sing (Apply Show_Sym0 t) Source # sShowList :: forall (t :: [Symbol]) (t :: Symbol). Sing t -> Sing t -> Sing (Apply (Apply ShowListSym0 t) t) Source #
PShow Symbol Source #
Instance details Defined in Data.Singletons.Prelude.Show Associated Types type ShowsPrec arg arg arg :: Symbol Source # type Show_ arg :: Symbol Source # type ShowList arg arg :: Symbol Source #
SMonoid Symbol Source #
Instance details Defined in Data.Singletons.Prelude.Monoid Methods sMempty :: Sing MemptySym0 Source # sMappend :: forall (t :: Symbol) (t :: Symbol). Sing t -> Sing t -> Sing (Apply (Apply MappendSym0 t) t) Source # sMconcat :: forall (t :: [Symbol]). Sing t -> Sing (Apply MconcatSym0 t) Source #
PMonoid Symbol Source #
Instance details Defined in Data.Singletons.Prelude.Monoid Associated Types type Mempty :: a Source # type Mappend arg arg :: a Source # type Mconcat arg :: a Source #
SIsString Symbol Source #
Instance details Defined in Data.Singletons.Prelude.IsString Methods sFromString :: forall (t :: Symbol). Sing t -> Sing (Apply FromStringSym0 t) Source #
PIsString Symbol Source #
Instance details Defined in Data.Singletons.Prelude.IsString Associated Types type FromString arg :: a Source #
KnownSymbol a => SingI (a :: Symbol)	Since: base-4.9.0.0
Instance details Defined in GHC.Generics Methods sing :: Sing a
KnownSymbol n => SingI (n :: Symbol) Source #
Instance details Defined in Data.Singletons.TypeLits.Internal Methods sing :: Sing n Source #
SingI t => SingI ('Text t :: ErrorMessage' Symbol) Source #
Instance details Defined in Data.Singletons.TypeError Methods sing :: Sing ('Text t) Source #
SingI ty => SingI ('ShowType ty :: ErrorMessage' Symbol) Source #
Instance details Defined in Data.Singletons.TypeError Methods sing :: Sing ('ShowType ty) Source #
(SingI e1, SingI e2) => SingI (e1 :<>: e2 :: ErrorMessage' Symbol) Source #
Instance details Defined in Data.Singletons.TypeError Methods sing :: Sing (e1 :<>: e2) Source #
(SingI e1, SingI e2) => SingI (e1 :$$: e2 :: ErrorMessage' Symbol) Source #
Instance details Defined in Data.Singletons.TypeError Methods sing :: Sing (e1 :$$: e2) Source #
SingI ShowParenSym0 Source #
Instance details Defined in Data.Singletons.Prelude.Show Methods sing :: Sing ShowParenSym0 Source #
SingI UnlinesSym0 Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing UnlinesSym0 Source #
SingI UnwordsSym0 Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing UnwordsSym0 Source #
SingI ShowSpaceSym0 Source #
Instance details Defined in Data.Singletons.Prelude.Show Methods sing :: Sing ShowSpaceSym0 Source #
SingI ShowCommaSpaceSym0 Source #
Instance details Defined in Data.Singletons.Prelude.Show Methods sing :: Sing ShowCommaSpaceSym0 Source #
SingI ShowCharSym0 Source #
Instance details Defined in Data.Singletons.Prelude.Show Methods sing :: Sing ShowCharSym0 Source #
SingI ShowStringSym0 Source #
Instance details Defined in Data.Singletons.Prelude.Show Methods sing :: Sing ShowStringSym0 Source #
SuppressUnusedWarnings ShowParenSym0 Source #
Instance details Defined in Data.Singletons.Prelude.Show Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings UnlinesSym0 Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings UnwordsSym0 Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings KnownSymbolSym0 Source #
Instance details Defined in Data.Singletons.TypeLits Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings ShowSpaceSym0 Source #
Instance details Defined in Data.Singletons.Prelude.Show Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings ShowCommaSpaceSym0 Source #
Instance details Defined in Data.Singletons.Prelude.Show Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings ShowCharSym0 Source #
Instance details Defined in Data.Singletons.Prelude.Show Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings ShowStringSym0 Source #
Instance details Defined in Data.Singletons.Prelude.Show Methods suppressUnusedWarnings :: () Source #
SingI (TypeErrorSym0 :: TyFun PErrorMessage a -> Type) Source #
Instance details Defined in Data.Singletons.TypeError Methods sing :: Sing TypeErrorSym0 Source #
SShow a => SingI (ShowListSym0 :: TyFun [a] (Symbol ~> Symbol) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Show Methods sing :: Sing ShowListSym0 Source #
SShow a => SingI (ShowsPrecSym0 :: TyFun Nat (a ~> (Symbol ~> Symbol)) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Show Methods sing :: Sing ShowsPrecSym0 Source #
SingI d => SingI (ShowCharSym1 d :: TyFun Symbol Symbol -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Show Methods sing :: Sing (ShowCharSym1 d) Source #
SingI d => SingI (ShowStringSym1 d :: TyFun Symbol Symbol -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Show Methods sing :: Sing (ShowStringSym1 d) Source #
SIsString a => SingI (FromStringSym0 :: TyFun Symbol a -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.IsString Methods sing :: Sing FromStringSym0 Source #
SingI (TextSym0 :: TyFun Symbol (ErrorMessage' Symbol) -> Type) Source #
Instance details Defined in Data.Singletons.TypeError Methods sing :: Sing TextSym0 Source #
SShow a => SingI (ShowsSym0 :: TyFun a (Symbol ~> Symbol) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Show Methods sing :: Sing ShowsSym0 Source #
SShow a => SingI (Show_Sym0 :: TyFun a Symbol -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Show Methods sing :: Sing Show_Sym0 Source #
SingI d => SingI (ShowParenSym1 d :: TyFun (Symbol ~> Symbol) (Symbol ~> Symbol) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Show Methods sing :: Sing (ShowParenSym1 d) Source #
SingI (ShowListWithSym0 :: TyFun (a ~> (Symbol ~> Symbol)) ([a] ~> (Symbol ~> Symbol)) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Show Methods sing :: Sing ShowListWithSym0 Source #
SingI ((:$$:@#@$) :: TyFun (ErrorMessage' Symbol) (ErrorMessage' Symbol ~> ErrorMessage' Symbol) -> Type) Source #
Instance details Defined in Data.Singletons.TypeError Methods sing :: Sing (:$$:@#@$) Source #
SingI ((:<>:@#@$) :: TyFun (ErrorMessage' Symbol) (ErrorMessage' Symbol ~> ErrorMessage' Symbol) -> Type) Source #
Instance details Defined in Data.Singletons.TypeError Methods sing :: Sing (:<>:@#@$) Source #
SuppressUnusedWarnings (ShowListSym0 :: TyFun [a] (Symbol ~> Symbol) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Show Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (ShowsPrecSym0 :: TyFun Nat (a ~> (Symbol ~> Symbol)) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Show Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (ShowCharSym1 a6989586621680279534 :: TyFun Symbol Symbol -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Show Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (ShowStringSym1 a6989586621680279523 :: TyFun Symbol Symbol -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Show Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (FromStringSym0 :: TyFun Symbol a -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.IsString Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (Show_Sym0 :: TyFun a Symbol -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Show Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (ShowsSym0 :: TyFun a (Symbol ~> Symbol) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Show Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (ShowParenSym1 a6989586621680279507 :: TyFun (Symbol ~> Symbol) (Symbol ~> Symbol) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Show Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (ShowListWithSym0 :: TyFun (a ~> (Symbol ~> Symbol)) ([a] ~> (Symbol ~> Symbol)) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Show Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (TypeErrorSym0 :: TyFun PErrorMessage a -> Type) Source #
Instance details Defined in Data.Singletons.TypeError Methods suppressUnusedWarnings :: () Source #
SingI d => SingI (ShowListWithSym1 d :: TyFun [a] (Symbol ~> Symbol) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Show Methods sing :: Sing (ShowListWithSym1 d) Source #
(SShow a, SingI d) => SingI (ShowListSym1 d :: TyFun Symbol Symbol -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Show Methods sing :: Sing (ShowListSym1 d) Source #
(SShow a, SingI d) => SingI (ShowsSym1 d :: TyFun Symbol Symbol -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Show Methods sing :: Sing (ShowsSym1 d) Source #
(SingI d1, SingI d2) => SingI (ShowParenSym2 d1 d2 :: TyFun Symbol Symbol -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Show Methods sing :: Sing (ShowParenSym2 d1 d2) Source #
SingI (ErrorSym0 :: TyFun Symbol a -> Type) Source #
Instance details Defined in Data.Singletons.TypeLits.Internal Methods sing :: Sing ErrorSym0 Source #
SingI (ErrorWithoutStackTraceSym0 :: TyFun Symbol a -> Type) Source #
Instance details Defined in Data.Singletons.TypeLits.Internal Methods sing :: Sing ErrorWithoutStackTraceSym0 Source #
(SShow a, SingI d) => SingI (ShowsPrecSym1 d :: TyFun a (Symbol ~> Symbol) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Show Methods sing :: Sing (ShowsPrecSym1 d) Source #
SingI (ShowTypeSym0 :: TyFun t (ErrorMessage' Symbol) -> Type) Source #
Instance details Defined in Data.Singletons.TypeError Methods sing :: Sing ShowTypeSym0 Source #
SingI x => SingI ((:$$:@#@$$) x :: TyFun (ErrorMessage' Symbol) (ErrorMessage' Symbol) -> Type) Source #
Instance details Defined in Data.Singletons.TypeError Methods sing :: Sing ((:$$:@#@$$) x) Source #
SingI x => SingI ((:<>:@#@$$) x :: TyFun (ErrorMessage' Symbol) (ErrorMessage' Symbol) -> Type) Source #
Instance details Defined in Data.Singletons.TypeError Methods sing :: Sing ((:<>:@#@$$) x) Source #
SuppressUnusedWarnings (ShowListWithSym1 a6989586621680279542 :: TyFun [a] (Symbol ~> Symbol) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Show Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (ShowListSym1 a6989586621680279577 :: TyFun Symbol Symbol -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Show Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (ShowsSym1 a6989586621680279560 :: TyFun Symbol Symbol -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Show Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (ShowParenSym2 a6989586621680279507 a6989586621680279508 :: TyFun Symbol Symbol -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Show Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (ShowsPrecSym1 a6989586621680279568 :: TyFun a (Symbol ~> Symbol) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Show Methods suppressUnusedWarnings :: () Source #
(SShow a, SingI d1, SingI d2) => SingI (ShowsPrecSym2 d1 d2 :: TyFun Symbol Symbol -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Show Methods sing :: Sing (ShowsPrecSym2 d1 d2) Source #
(SingI d1, SingI d2) => SingI (ShowListWithSym2 d1 d2 :: TyFun Symbol Symbol -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Show Methods sing :: Sing (ShowListWithSym2 d1 d2) Source #
SuppressUnusedWarnings (ShowsPrecSym2 a6989586621680279568 a6989586621680279569 :: TyFun Symbol Symbol -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Show Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (ShowListWithSym2 a6989586621680279542 a6989586621680279543 :: TyFun Symbol Symbol -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Show Methods suppressUnusedWarnings :: () Source #
data Sing (s :: Symbol)
Instance details Defined in GHC.Generics data Sing (s :: Symbol) where SSym :: forall (s :: Symbol). KnownSymbol s => Sing s
type DemoteRep Symbol
Instance details Defined in GHC.Generics type DemoteRep Symbol = String
type Demote Symbol Source #
Instance details Defined in Data.Singletons.TypeLits.Internal type Demote Symbol = Text
type Demote PErrorMessage Source #
Instance details Defined in Data.Singletons.TypeError type Demote PErrorMessage = ErrorMessage
type Sing Source #
Instance details Defined in Data.Singletons.TypeLits.Internal type Sing = SSymbol
type Sing Source #
Instance details Defined in Data.Singletons.TypeError type Sing = SErrorMessage
type Mempty Source #
Instance details Defined in Data.Singletons.Prelude.Monoid type Mempty
type Sconcat (arg :: NonEmpty Symbol) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type Sconcat (arg :: NonEmpty Symbol)
type Show_ (arg :: Symbol) Source #
Instance details Defined in Data.Singletons.Prelude.Show type Show_ (arg :: Symbol)
type Mconcat (arg :: [Symbol]) Source #
Instance details Defined in Data.Singletons.Prelude.Monoid type Mconcat (arg :: [Symbol])
type FromString a Source #
Instance details Defined in Data.Singletons.Prelude.IsString type FromString a = a
type (x :: Symbol) == (y :: Symbol) Source #
Instance details Defined in Data.Singletons.TypeLits.Internal type (x :: Symbol) == (y :: Symbol) = DefaultEq x y
type (x :: Symbol) /= (y :: Symbol) Source #
Instance details Defined in Data.Singletons.TypeLits.Internal type (x :: Symbol) /= (y :: Symbol) = Not (x == y)
type Compare (a :: Symbol) (b :: Symbol) Source #
Instance details Defined in Data.Singletons.TypeLits.Internal type Compare (a :: Symbol) (b :: Symbol) = CmpSymbol a b
type (arg1 :: Symbol) < (arg2 :: Symbol) Source #
Instance details Defined in Data.Singletons.TypeLits.Internal type (arg1 :: Symbol) < (arg2 :: Symbol)
type (arg1 :: Symbol) <= (arg2 :: Symbol) Source #
Instance details Defined in Data.Singletons.TypeLits.Internal type (arg1 :: Symbol) <= (arg2 :: Symbol)
type (arg1 :: Symbol) > (arg2 :: Symbol) Source #
Instance details Defined in Data.Singletons.TypeLits.Internal type (arg1 :: Symbol) > (arg2 :: Symbol)
type (arg1 :: Symbol) >= (arg2 :: Symbol) Source #
Instance details Defined in Data.Singletons.TypeLits.Internal type (arg1 :: Symbol) >= (arg2 :: Symbol)
type Max (arg1 :: Symbol) (arg2 :: Symbol) Source #
Instance details Defined in Data.Singletons.TypeLits.Internal type Max (arg1 :: Symbol) (arg2 :: Symbol)
type Min (arg1 :: Symbol) (arg2 :: Symbol) Source #
Instance details Defined in Data.Singletons.TypeLits.Internal type Min (arg1 :: Symbol) (arg2 :: Symbol)
type (a :: Symbol) <> (b :: Symbol) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type (a :: Symbol) <> (b :: Symbol) = AppendSymbol a b
type ShowList (arg1 :: [Symbol]) arg2 Source #
Instance details Defined in Data.Singletons.Prelude.Show type ShowList (arg1 :: [Symbol]) arg2
type Mappend (arg1 :: Symbol) (arg2 :: Symbol) Source #
Instance details Defined in Data.Singletons.Prelude.Monoid type Mappend (arg1 :: Symbol) (arg2 :: Symbol)
type Apply KnownSymbolSym0 (a6989586621679491990 :: Symbol) Source #
Instance details Defined in Data.Singletons.TypeLits type Apply KnownSymbolSym0 (a6989586621679491990 :: Symbol) = KnownSymbolSym1 a6989586621679491990
type Apply ShowSpaceSym0 (a6989586621680279495 :: Symbol) Source #
Instance details Defined in Data.Singletons.Prelude.Show type Apply ShowSpaceSym0 (a6989586621680279495 :: Symbol) = ShowSpaceSym1 a6989586621680279495
type Apply ShowCommaSpaceSym0 (a6989586621680279489 :: Symbol) Source #
Instance details Defined in Data.Singletons.Prelude.Show type Apply ShowCommaSpaceSym0 (a6989586621680279489 :: Symbol) = ShowCommaSpaceSym1 a6989586621680279489
type ShowsPrec a1 (a2 :: Symbol) a3 Source #
Instance details Defined in Data.Singletons.Prelude.Show type ShowsPrec a1 (a2 :: Symbol) a3
type Apply (ShowCharSym1 a6989586621680279534 :: TyFun Symbol Symbol -> Type) (a6989586621680279535 :: Symbol) Source #
Instance details Defined in Data.Singletons.Prelude.Show type Apply (ShowCharSym1 a6989586621680279534 :: TyFun Symbol Symbol -> Type) (a6989586621680279535 :: Symbol) = ShowCharSym2 a6989586621680279534 a6989586621680279535
type Apply (ShowStringSym1 a6989586621680279523 :: TyFun Symbol Symbol -> Type) (a6989586621680279524 :: Symbol) Source #
Instance details Defined in Data.Singletons.Prelude.Show type Apply (ShowStringSym1 a6989586621680279523 :: TyFun Symbol Symbol -> Type) (a6989586621680279524 :: Symbol) = ShowStringSym2 a6989586621680279523 a6989586621680279524
type Apply (FromStringSym0 :: TyFun Symbol k2 -> Type) (a6989586621681280469 :: Symbol) Source #
Instance details Defined in Data.Singletons.Prelude.IsString type Apply (FromStringSym0 :: TyFun Symbol k2 -> Type) (a6989586621681280469 :: Symbol) = FromStringSym1 a6989586621681280469 :: k2
type Apply (Show_Sym0 :: TyFun a Symbol -> Type) (a6989586621680279573 :: a) Source #
Instance details Defined in Data.Singletons.Prelude.Show type Apply (Show_Sym0 :: TyFun a Symbol -> Type) (a6989586621680279573 :: a) = Show_Sym1 a6989586621680279573
type Apply (TypeErrorSym0 :: TyFun PErrorMessage k2 -> Type) (a6989586621681349593 :: PErrorMessage) Source #
Instance details Defined in Data.Singletons.TypeError type Apply (TypeErrorSym0 :: TyFun PErrorMessage k2 -> Type) (a6989586621681349593 :: PErrorMessage) = TypeErrorSym1 a6989586621681349593 :: k2
type Apply (ShowListSym1 a6989586621680279577 :: TyFun Symbol Symbol -> Type) (a6989586621680279578 :: Symbol) Source #
Instance details Defined in Data.Singletons.Prelude.Show type Apply (ShowListSym1 a6989586621680279577 :: TyFun Symbol Symbol -> Type) (a6989586621680279578 :: Symbol) = ShowListSym2 a6989586621680279577 a6989586621680279578
type Apply (ShowsSym1 a6989586621680279560 :: TyFun Symbol Symbol -> Type) (a6989586621680279561 :: Symbol) Source #
Instance details Defined in Data.Singletons.Prelude.Show type Apply (ShowsSym1 a6989586621680279560 :: TyFun Symbol Symbol -> Type) (a6989586621680279561 :: Symbol) = ShowsSym2 a6989586621680279560 a6989586621680279561
type Apply (ShowParenSym2 a6989586621680279507 a6989586621680279508 :: TyFun Symbol Symbol -> Type) (a6989586621680279509 :: Symbol) Source #
Instance details Defined in Data.Singletons.Prelude.Show type Apply (ShowParenSym2 a6989586621680279507 a6989586621680279508 :: TyFun Symbol Symbol -> Type) (a6989586621680279509 :: Symbol)
type Apply (ShowsPrecSym2 a6989586621680279568 a6989586621680279569 :: TyFun Symbol Symbol -> Type) (a6989586621680279570 :: Symbol) Source #
Instance details Defined in Data.Singletons.Prelude.Show type Apply (ShowsPrecSym2 a6989586621680279568 a6989586621680279569 :: TyFun Symbol Symbol -> Type) (a6989586621680279570 :: Symbol) = ShowsPrecSym3 a6989586621680279568 a6989586621680279569 a6989586621680279570
type Apply (ShowListWithSym2 a6989586621680279542 a6989586621680279543 :: TyFun Symbol Symbol -> Type) (a6989586621680279544 :: Symbol) Source #
Instance details Defined in Data.Singletons.Prelude.Show type Apply (ShowListWithSym2 a6989586621680279542 a6989586621680279543 :: TyFun Symbol Symbol -> Type) (a6989586621680279544 :: Symbol) = ShowListWithSym3 a6989586621680279542 a6989586621680279543 a6989586621680279544
type Apply ShowParenSym0 (a6989586621680279507 :: Bool) Source #
Instance details Defined in Data.Singletons.Prelude.Show type Apply ShowParenSym0 (a6989586621680279507 :: Bool) = ShowParenSym1 a6989586621680279507
type Apply ShowCharSym0 (a6989586621680279534 :: Symbol) Source #
Instance details Defined in Data.Singletons.Prelude.Show type Apply ShowCharSym0 (a6989586621680279534 :: Symbol) = ShowCharSym1 a6989586621680279534
type Apply ShowStringSym0 (a6989586621680279523 :: Symbol) Source #
Instance details Defined in Data.Singletons.Prelude.Show type Apply ShowStringSym0 (a6989586621680279523 :: Symbol) = ShowStringSym1 a6989586621680279523
type Apply (ShowsPrecSym0 :: TyFun Nat (a ~> (Symbol ~> Symbol)) -> Type) (a6989586621680279568 :: Nat) Source #
Instance details Defined in Data.Singletons.Prelude.Show type Apply (ShowsPrecSym0 :: TyFun Nat (a ~> (Symbol ~> Symbol)) -> Type) (a6989586621680279568 :: Nat) = ShowsPrecSym1 a6989586621680279568 :: TyFun a (Symbol ~> Symbol) -> Type
type Apply (ShowsSym0 :: TyFun a (Symbol ~> Symbol) -> Type) (a6989586621680279560 :: a) Source #
Instance details Defined in Data.Singletons.Prelude.Show type Apply (ShowsSym0 :: TyFun a (Symbol ~> Symbol) -> Type) (a6989586621680279560 :: a) = ShowsSym1 a6989586621680279560
type Apply (ShowsPrecSym1 a6989586621680279568 :: TyFun a (Symbol ~> Symbol) -> Type) (a6989586621680279569 :: a) Source #
Instance details Defined in Data.Singletons.Prelude.Show type Apply (ShowsPrecSym1 a6989586621680279568 :: TyFun a (Symbol ~> Symbol) -> Type) (a6989586621680279569 :: a) = ShowsPrecSym2 a6989586621680279568 a6989586621680279569
type Apply UnlinesSym0 (a6989586621679969412 :: [Symbol]) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal type Apply UnlinesSym0 (a6989586621679969412 :: [Symbol]) = UnlinesSym1 a6989586621679969412
type Apply UnwordsSym0 (a6989586621679969402 :: [Symbol]) Source #
Instance details Defined in Data.Singletons.Prelude.List.Internal type Apply UnwordsSym0 (a6989586621679969402 :: [Symbol]) = UnwordsSym1 a6989586621679969402
type Apply (ShowListSym0 :: TyFun [a] (Symbol ~> Symbol) -> Type) (a6989586621680279577 :: [a]) Source #
Instance details Defined in Data.Singletons.Prelude.Show type Apply (ShowListSym0 :: TyFun [a] (Symbol ~> Symbol) -> Type) (a6989586621680279577 :: [a]) = ShowListSym1 a6989586621680279577
type Apply (ShowListWithSym1 a6989586621680279542 :: TyFun [a] (Symbol ~> Symbol) -> Type) (a6989586621680279543 :: [a]) Source #
Instance details Defined in Data.Singletons.Prelude.Show type Apply (ShowListWithSym1 a6989586621680279542 :: TyFun [a] (Symbol ~> Symbol) -> Type) (a6989586621680279543 :: [a]) = ShowListWithSym2 a6989586621680279542 a6989586621680279543
type Apply (ShowParenSym1 a6989586621680279507 :: TyFun (Symbol ~> Symbol) (Symbol ~> Symbol) -> Type) (a6989586621680279508 :: Symbol ~> Symbol) Source #
Instance details Defined in Data.Singletons.Prelude.Show type Apply (ShowParenSym1 a6989586621680279507 :: TyFun (Symbol ~> Symbol) (Symbol ~> Symbol) -> Type) (a6989586621680279508 :: Symbol ~> Symbol) = ShowParenSym2 a6989586621680279507 a6989586621680279508
type Apply (ShowListWithSym0 :: TyFun (a ~> (Symbol ~> Symbol)) ([a] ~> (Symbol ~> Symbol)) -> Type) (a6989586621680279542 :: a ~> (Symbol ~> Symbol)) Source #
Instance details Defined in Data.Singletons.Prelude.Show type Apply (ShowListWithSym0 :: TyFun (a ~> (Symbol ~> Symbol)) ([a] ~> (Symbol ~> Symbol)) -> Type) (a6989586621680279542 :: a ~> (Symbol ~> Symbol)) = ShowListWithSym1 a6989586621680279542

type family Sing Source #

The singleton kind-indexed type family.

Instances

Instances details

type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = SBool
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = SOrdering
type Sing Source #
Instance details Defined in Data.Singletons.TypeLits.Internal type Sing = SNat
type Sing Source #
Instance details Defined in Data.Singletons.TypeLits.Internal type Sing = SSymbol
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = STuple0
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = SVoid
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type Sing = SAll
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type Sing = SAny
type Sing Source #
Instance details Defined in Data.Singletons.TypeError type Sing = SErrorMessage
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = SList :: [a] -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = SMaybe :: Maybe a -> Type
type Sing Source #	A choice of singleton for the kind `TYPE rep` (for some `RuntimeRep` `rep`), an instantiation of which is the famous kind `Type`. Conceivably, one could generalize this instance to `Sing @k` for any kind `k`, and remove all other `Sing` instances. We don't adopt this design, however, since it is far more convenient in practice to work with explicit singleton values than `TypeRep`s (for instance, `TypeRep`s are more difficult to pattern match on, and require extra runtime checks). We cannot produce explicit singleton values for everything in `TYPE rep`, however, since it is an open kind, so we reach for `TypeRep` in this one particular case.
Instance details Defined in Data.Singletons.TypeRepTYPE type Sing = TypeRep :: TYPE rep -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type Sing = SMin :: Min a -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type Sing = SMax :: Max a -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type Sing = SFirst :: First a -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type Sing = SLast :: Last a -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type Sing = SWrappedMonoid :: WrappedMonoid m -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type Sing = SOption :: Option a -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = SIdentity :: Identity a -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Monoid type Sing = SFirst :: First a -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Monoid type Sing = SLast :: Last a -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type Sing = SDual :: Dual a -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type Sing = SSum :: Sum a -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type Sing = SProduct :: Product a -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Ord type Sing = SDown :: Down a -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = SNonEmpty :: NonEmpty a -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = SEither :: Either a b -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = STuple2 :: (a, b) -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup type Sing = SArg :: Arg a b -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Proxy type Sing = SProxy :: Proxy t -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Internal type Sing = SLambda :: (k1 ~> k2) -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Internal type Sing = SWrappedSing :: WrappedSing a -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Sigma type Sing = SSigma :: Sigma s t -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = STuple3 :: (a, b, c) -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Const type Sing = SConst :: Const a b -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = STuple4 :: (a, b, c, d) -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = STuple5 :: (a, b, c, d, e) -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = STuple6 :: (a, b, c, d, e, f) -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = STuple7 :: (a, b, c, d, e, f, g) -> Type

data SNat n Source #

Constructors

KnownNat n => SNat

Instances

Instances details

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

data SSymbol n Source #

Constructors

KnownSymbol n => SSym

Instances

Instances details

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

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

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

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

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

type family Error str 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 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 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.Singletons.Prelude.Ord, and not the <= from GHC.TypeNats. The latter is simply a type alias for (a <=? b) ~ 'True.)

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

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

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

Since: base-4.11.0.0

sLog2 :: Sing x -> Sing (Log2 x) 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 a 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 a where ... infixl 7 Source #

Equations

Quot a_6989586621679493485 a_6989586621679493487 = Apply (Apply DivSym0 a_6989586621679493485) a_6989586621679493487

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

type family Rem a a where ... infixl 7 Source #

Equations

Rem a_6989586621679493474 a_6989586621679493476 = Apply (Apply ModSym0 a_6989586621679493474) a_6989586621679493476

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

type family QuotRem a a where ... Source #

Equations

QuotRem a_6989586621679493496 a_6989586621679493498 = Apply (Apply DivModSym0 a_6989586621679493496) a_6989586621679493498

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

Defunctionalization symbols

data ErrorSym0 a6989586621679472252 Source #

Instances

Instances details

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

type ErrorSym1 (a6989586621679472252 :: k0) = Error a6989586621679472252 :: k Source #

data ErrorWithoutStackTraceSym0 a6989586621679472488 Source #

Instances

Instances details

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

type ErrorWithoutStackTraceSym1 (a6989586621679472488 :: k0) = ErrorWithoutStackTrace a6989586621679472488 :: k Source #

type UndefinedSym0 = Undefined :: k Source #

data KnownNatSym0 a6989586621679491988 Source #

Instances

Instances details

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

type KnownNatSym1 (a6989586621679491988 :: Nat) = KnownNat a6989586621679491988 :: Constraint Source #

data KnownSymbolSym0 a6989586621679491990 Source #

Instances

Instances details

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

type KnownSymbolSym1 (a6989586621679491990 :: Symbol) = KnownSymbol a6989586621679491990 :: Constraint Source #

data (^@#@$) a6989586621679472866 infixr 8 Source #

Instances

Instances details

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

data a6989586621679472866 ^@#@$$ a6989586621679472867 infixr 8 Source #

Instances

Instances details

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

type (^@#@$$$) (a6989586621679472866 :: Nat) (a6989586621679472867 :: Nat) = (^) a6989586621679472866 a6989586621679472867 :: Nat infixr 8 Source #

data (<=?@#@$) a6989586621679473158 infix 4 Source #

Instances

Instances details

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

data a6989586621679473158 <=?@#@$$ a6989586621679473159 infix 4 Source #

Instances

Instances details

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

type (<=?@#@$$$) (a6989586621679473158 :: Nat) (a6989586621679473159 :: Nat) = (<=?) a6989586621679473158 a6989586621679473159 :: Bool infix 4 Source #

data Log2Sym0 a6989586621679492472 Source #

Instances

Instances details

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

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

data DivSym0 a6989586621679492680 infixl 7 Source #

Instances

Instances details

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

data DivSym1 a6989586621679492680 a6989586621679492681 infixl 7 Source #

Instances

Instances details

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

type DivSym2 (a6989586621679492680 :: Nat) (a6989586621679492681 :: Nat) = Div a6989586621679492680 a6989586621679492681 :: Nat infixl 7 Source #

data ModSym0 a6989586621679493016 infixl 7 Source #

Instances

Instances details

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

data ModSym1 a6989586621679493016 a6989586621679493017 infixl 7 Source #

Instances

Instances details

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

type ModSym2 (a6989586621679493016 :: Nat) (a6989586621679493017 :: Nat) = Mod a6989586621679493016 a6989586621679493017 :: Nat infixl 7 Source #

data DivModSym0 a6989586621679493510 Source #

Instances

Instances details

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

data DivModSym1 a6989586621679493510 a6989586621679493511 Source #

Instances

Instances details

SuppressUnusedWarnings (DivModSym1 a6989586621679493510 :: TyFun Nat (Nat, Nat) -> Type) Source #
Instance details Defined in Data.Singletons.TypeLits Methods suppressUnusedWarnings :: () Source #
type Apply (DivModSym1 a6989586621679493510 :: TyFun Nat (Nat, Nat) -> Type) (a6989586621679493511 :: Nat) Source #
Instance details Defined in Data.Singletons.TypeLits type Apply (DivModSym1 a6989586621679493510 :: TyFun Nat (Nat, Nat) -> Type) (a6989586621679493511 :: Nat) = DivModSym2 a6989586621679493510 a6989586621679493511

type DivModSym2 (a6989586621679493510 :: Nat) (a6989586621679493511 :: Nat) = DivMod a6989586621679493510 a6989586621679493511 :: (Nat, Nat) Source #

data QuotSym0 a6989586621679493492 infixl 7 Source #

Instances

Instances details

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

data QuotSym1 a6989586621679493492 a6989586621679493493 infixl 7 Source #

Instances

Instances details

SuppressUnusedWarnings (QuotSym1 a6989586621679493492 :: TyFun Nat Nat -> Type) Source #
Instance details Defined in Data.Singletons.TypeLits Methods suppressUnusedWarnings :: () Source #
type Apply (QuotSym1 a6989586621679493492 :: TyFun Nat Nat -> Type) (a6989586621679493493 :: Nat) Source #
Instance details Defined in Data.Singletons.TypeLits type Apply (QuotSym1 a6989586621679493492 :: TyFun Nat Nat -> Type) (a6989586621679493493 :: Nat) = QuotSym2 a6989586621679493492 a6989586621679493493

type QuotSym2 (a6989586621679493492 :: Nat) (a6989586621679493493 :: Nat) = Quot a6989586621679493492 a6989586621679493493 :: Nat infixl 7 Source #

data RemSym0 a6989586621679493481 infixl 7 Source #

Instances

Instances details

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

data RemSym1 a6989586621679493481 a6989586621679493482 infixl 7 Source #

Instances

Instances details

SuppressUnusedWarnings (RemSym1 a6989586621679493481 :: TyFun Nat Nat -> Type) Source #
Instance details Defined in Data.Singletons.TypeLits Methods suppressUnusedWarnings :: () Source #
type Apply (RemSym1 a6989586621679493481 :: TyFun Nat Nat -> Type) (a6989586621679493482 :: Nat) Source #
Instance details Defined in Data.Singletons.TypeLits type Apply (RemSym1 a6989586621679493481 :: TyFun Nat Nat -> Type) (a6989586621679493482 :: Nat) = RemSym2 a6989586621679493481 a6989586621679493482

type RemSym2 (a6989586621679493481 :: Nat) (a6989586621679493482 :: Nat) = Rem a6989586621679493481 a6989586621679493482 :: Nat infixl 7 Source #

data QuotRemSym0 a6989586621679493503 Source #

Instances

Instances details

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

data QuotRemSym1 a6989586621679493503 a6989586621679493504 Source #

Instances

Instances details

SuppressUnusedWarnings (QuotRemSym1 a6989586621679493503 :: TyFun Nat (Nat, Nat) -> Type) Source #
Instance details Defined in Data.Singletons.TypeLits Methods suppressUnusedWarnings :: () Source #
type Apply (QuotRemSym1 a6989586621679493503 :: TyFun Nat (Nat, Nat) -> Type) (a6989586621679493504 :: Nat) Source #
Instance details Defined in Data.Singletons.TypeLits type Apply (QuotRemSym1 a6989586621679493503 :: TyFun Nat (Nat, Nat) -> Type) (a6989586621679493504 :: Nat) = QuotRemSym2 a6989586621679493503 a6989586621679493504

type QuotRemSym2 (a6989586621679493503 :: Nat) (a6989586621679493504 :: Nat) = QuotRem a6989586621679493503 a6989586621679493504 :: (Nat, Nat) Source #

Orphan instances

Enum Nat Source #
Instance details Methods succ :: Nat -> Nat # pred :: Nat -> Nat # toEnum :: Int -> Nat # fromEnum :: Nat -> Int # enumFrom :: Nat -> [Nat] # enumFromThen :: Nat -> Nat -> [Nat] # enumFromTo :: Nat -> Nat -> [Nat] # enumFromThenTo :: Nat -> Nat -> Nat -> [Nat] #
Eq Nat Source #
Instance details Methods (==) :: Nat -> Nat -> Bool # (/=) :: Nat -> Nat -> Bool #
Eq Symbol Source #	This bogus instance is helpful for people who want to define functions over Symbols that will only be used at the type level or as singletons.
Instance details Methods (==) :: Symbol -> Symbol -> Bool # (/=) :: Symbol -> Symbol -> Bool #
Num Nat Source #	This bogus `Num` instance is helpful for people who want to define functions over Nats that will only be used at the type level or as singletons. A correct SNum instance for Nat singletons exists.
Instance details Methods (+) :: Nat -> Nat -> Nat # (-) :: Nat -> Nat -> Nat # (*) :: Nat -> Nat -> Nat # negate :: Nat -> Nat # abs :: Nat -> Nat # signum :: Nat -> Nat # fromInteger :: Integer -> Nat #
Ord Nat Source #
Instance details Methods compare :: Nat -> Nat -> Ordering # (<) :: Nat -> Nat -> Bool # (<=) :: Nat -> Nat -> Bool # (>) :: Nat -> Nat -> Bool # (>=) :: Nat -> Nat -> Bool # max :: Nat -> Nat -> Nat # min :: Nat -> Nat -> Nat #
Ord Symbol Source #
Instance details Methods compare :: Symbol -> Symbol -> Ordering # (<) :: Symbol -> Symbol -> Bool # (<=) :: Symbol -> Symbol -> Bool # (>) :: Symbol -> Symbol -> Bool # (>=) :: Symbol -> Symbol -> Bool # max :: Symbol -> Symbol -> Symbol # min :: Symbol -> Symbol -> Symbol #
Show Nat Source #
Instance details Methods showsPrec :: Int -> Nat -> ShowS # show :: Nat -> String # showList :: [Nat] -> ShowS #
Show Symbol Source #
Instance details Methods showsPrec :: Int -> Symbol -> ShowS # show :: Symbol -> String # showList :: [Symbol] -> ShowS #
IsString Symbol Source #
Instance details Methods fromString :: String -> Symbol #
Semigroup Symbol Source #
Instance details Methods (<>) :: Symbol -> Symbol -> Symbol # sconcat :: NonEmpty Symbol -> Symbol # stimes :: Integral b => b -> Symbol -> Symbol #
Monoid Symbol Source #
Instance details Methods mempty :: Symbol # mappend :: Symbol -> Symbol -> Symbol # mconcat :: [Symbol] -> Symbol #