singletons-2.6: A framework for generating singleton types
Copyright(C) 2014 Richard Eisenberg
LicenseBSD-style (see LICENSE)
MaintainerRyan Scott
Stabilityexperimental
Portabilitynon-portable
Safe HaskellNone
LanguageHaskell2010

Data.Singletons.TypeLits

Description

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

Synopsis

Documentation

data Nat #

Instances

Instances details
Enum Nat 
Instance details

Defined in Data.Singletons.TypeLits

Methods

succ :: Nat -> Nat

pred :: Nat -> Nat

toEnum :: Int -> Nat

fromEnum :: Nat -> Int

enumFrom :: Nat -> [Nat]

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

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

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

Eq Nat 
Instance details

Defined in Data.Singletons.TypeLits

Methods

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

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

Num Nat

This bogus Num instance is helpful for people who want to define functions over Nats that will only be used at the type level or as singletons. A correct SNum instance for Nat singletons exists.

Instance details

Defined in Data.Singletons.TypeLits

Methods

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

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

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

negate :: Nat -> Nat

abs :: Nat -> Nat

signum :: Nat -> Nat

fromInteger :: Integer -> Nat

Ord Nat 
Instance details

Defined in Data.Singletons.TypeLits

Methods

compare :: Nat -> Nat -> Ordering

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

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

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

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

max :: Nat -> Nat -> Nat

min :: Nat -> Nat -> Nat

Show Nat 
Instance details

Defined in Data.Singletons.TypeLits

Methods

showsPrec :: Int -> Nat -> ShowS

show :: Nat -> String

showList :: [Nat] -> ShowS

SingKind Nat Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

Associated Types

type Demote Nat = (r :: Type) Source #

Methods

fromSing :: forall (a :: Nat). Sing a -> Demote Nat Source #

toSing :: Demote Nat -> SomeSing Nat Source #

SDecide Nat Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

Methods

(%~) :: forall (a :: Nat) (b :: Nat). Sing a -> Sing b -> Decision (a :~: b) Source #

PEq Nat Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

Associated Types

type x == y :: Bool Source #

type x /= y :: Bool Source #

SEq Nat Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

Methods

(%==) :: forall (a :: Nat) (b :: Nat). Sing a -> Sing b -> Sing (a == b) Source #

(%/=) :: forall (a :: Nat) (b :: Nat). Sing a -> Sing b -> Sing (a /= b) Source #

SOrd Nat Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

Methods

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

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

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

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

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

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

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

POrd Nat Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

Associated Types

type Compare arg arg :: Ordering Source #

type arg < arg :: Bool Source #

type arg <= arg :: Bool Source #

type arg > arg :: Bool Source #

type arg >= arg :: Bool Source #

type Max arg arg :: a Source #

type Min arg arg :: a Source #

SNum Nat Source # 
Instance details

Defined in Data.Singletons.Prelude.Num

Methods

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

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

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

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

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

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

sFromInteger :: forall (t :: Nat). Sing t -> Sing (Apply FromIntegerSym0 t) Source #

PNum Nat Source # 
Instance details

Defined in Data.Singletons.Prelude.Num

Associated Types

type arg + arg :: a Source #

type arg - arg :: a Source #

type arg * arg :: a Source #

type Negate arg :: a Source #

type Abs arg :: a Source #

type Signum arg :: a Source #

type FromInteger arg :: a Source #

SEnum Nat Source # 
Instance details

Defined in Data.Singletons.Prelude.Enum

Methods

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

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

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

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

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

sEnumFromThenTo :: forall (t :: Nat) (t :: Nat) (t :: Nat). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply EnumFromThenToSym0 t) t) t) Source #

PEnum Nat Source # 
Instance details

Defined in Data.Singletons.Prelude.Enum

Associated Types

type Succ arg :: a Source #

type Pred arg :: a Source #

type ToEnum arg :: a Source #

type FromEnum arg :: Nat Source #

type EnumFromTo arg arg :: [a] Source #

type EnumFromThenTo arg arg arg :: [a] Source #

SShow Nat Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

Methods

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

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

sShowList :: forall (t :: [Nat]) (t :: Symbol). Sing t -> Sing t -> Sing (Apply (Apply ShowListSym0 t) t) Source #

PShow Nat Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

Associated Types

type ShowsPrec arg arg arg :: Symbol Source #

type Show_ arg :: Symbol Source #

type ShowList arg arg :: Symbol Source #

KnownNat n => SingI (n :: Nat) Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

Methods

sing :: Sing n Source #

SingI Log2Sym0 Source # 
Instance details

Defined in Data.Singletons.TypeLits

Methods

sing :: Sing Log2Sym0 Source #

SingI (<=?@#@$) Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

Methods

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

SingI (^@#@$) Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

Methods

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

SingI DivSym0 Source # 
Instance details

Defined in Data.Singletons.TypeLits

Methods

sing :: Sing DivSym0 Source #

SingI ModSym0 Source # 
Instance details

Defined in Data.Singletons.TypeLits

Methods

sing :: Sing ModSym0 Source #

SuppressUnusedWarnings KnownNatSym0 Source # 
Instance details

Defined in Data.Singletons.TypeLits

Methods

suppressUnusedWarnings :: () Source #

SuppressUnusedWarnings Log2Sym0 Source # 
Instance details

Defined in Data.Singletons.TypeLits

Methods

suppressUnusedWarnings :: () Source #

SuppressUnusedWarnings (<=?@#@$) Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

Methods

suppressUnusedWarnings :: () Source #

SuppressUnusedWarnings (^@#@$) Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

Methods

suppressUnusedWarnings :: () Source #

SuppressUnusedWarnings DivSym0 Source # 
Instance details

Defined in Data.Singletons.TypeLits

Methods

suppressUnusedWarnings :: () Source #

SuppressUnusedWarnings ModSym0 Source # 
Instance details

Defined in Data.Singletons.TypeLits

Methods

suppressUnusedWarnings :: () Source #

SuppressUnusedWarnings QuotSym0 Source # 
Instance details

Defined in Data.Singletons.TypeLits

Methods

suppressUnusedWarnings :: () Source #

SuppressUnusedWarnings RemSym0 Source # 
Instance details

Defined in Data.Singletons.TypeLits

Methods

suppressUnusedWarnings :: () Source #

SuppressUnusedWarnings DivModSym0 Source # 
Instance details

Defined in Data.Singletons.TypeLits

Methods

suppressUnusedWarnings :: () Source #

SuppressUnusedWarnings QuotRemSym0 Source # 
Instance details

Defined in Data.Singletons.TypeLits

Methods

suppressUnusedWarnings :: () Source #

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

Defined in Data.Singletons.TypeLits.Internal

Methods

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

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

Defined in Data.Singletons.TypeLits.Internal

Methods

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

SingI x => SingI (DivSym1 x :: TyFun Nat Nat -> Type) Source # 
Instance details

Defined in Data.Singletons.TypeLits

Methods

sing :: Sing (DivSym1 x) Source #

SingI x => SingI (ModSym1 x :: TyFun Nat Nat -> Type) Source # 
Instance details

Defined in Data.Singletons.TypeLits

Methods

sing :: Sing (ModSym1 x) Source #

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

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

SNum a => SingI (FromIntegerSym0 :: TyFun Nat a -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Num

Methods

sing :: Sing FromIntegerSym0 Source #

SEnum a => SingI (ToEnumSym0 :: TyFun Nat a -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Enum

Methods

sing :: Sing ToEnumSym0 Source #

SingI (SplitAtSym0 :: TyFun Nat ([a] ~> ([a], [a])) -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing SplitAtSym0 Source #

SingI (DropSym0 :: TyFun Nat ([a] ~> [a]) -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing DropSym0 Source #

SingI (TakeSym0 :: TyFun Nat ([a] ~> [a]) -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing TakeSym0 Source #

SingI (ReplicateSym0 :: TyFun Nat (a ~> [a]) -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing ReplicateSym0 Source #

SShow a => SingI (ShowsPrecSym0 :: TyFun Nat (a ~> (Symbol ~> Symbol)) -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing ShowsPrecSym0 Source #

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

Defined in Data.Singletons.Prelude.List.NonEmpty

Methods

sing :: Sing SplitAtSym0 Source #

SingI (DropSym0 :: TyFun Nat (NonEmpty a ~> [a]) -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.List.NonEmpty

Methods

sing :: Sing DropSym0 Source #

SingI (TakeSym0 :: TyFun Nat (NonEmpty a ~> [a]) -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.List.NonEmpty

Methods

sing :: Sing TakeSym0 Source #

SEnum a => SingI (FromEnumSym0 :: TyFun a Nat -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Enum

Methods

sing :: Sing FromEnumSym0 Source #

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing ElemIndicesSym0 Source #

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing ElemIndexSym0 Source #

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

Defined in Data.Singletons.Prelude.List.NonEmpty

Methods

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

SingI (LengthSym0 :: TyFun (NonEmpty a) Nat -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.List.NonEmpty

Methods

sing :: Sing LengthSym0 Source #

SingI (FindIndicesSym0 :: TyFun (a ~> Bool) ([a] ~> [Nat]) -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing FindIndicesSym0 Source #

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing FindIndexSym0 Source #

SuppressUnusedWarnings ((!!@#@$) :: TyFun [a6989586621679970139] (Nat ~> a6989586621679970139) -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

suppressUnusedWarnings :: () Source #

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

Defined in Data.Singletons.TypeLits.Internal

Methods

suppressUnusedWarnings :: () Source #

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

Defined in Data.Singletons.TypeLits.Internal

Methods

suppressUnusedWarnings :: () Source #

SuppressUnusedWarnings (DivSym1 a3530822107858468865 :: TyFun Nat Nat -> Type) Source # 
Instance details

Defined in Data.Singletons.TypeLits

Methods

suppressUnusedWarnings :: () Source #

SuppressUnusedWarnings (ModSym1 a3530822107858468865 :: TyFun Nat Nat -> Type) Source # 
Instance details

Defined in Data.Singletons.TypeLits

Methods

suppressUnusedWarnings :: () Source #

SuppressUnusedWarnings (QuotSym1 a6989586621679504151 :: TyFun Nat Nat -> Type) Source # 
Instance details

Defined in Data.Singletons.TypeLits

Methods

suppressUnusedWarnings :: () Source #

SuppressUnusedWarnings (RemSym1 a6989586621679504141 :: TyFun Nat Nat -> Type) Source # 
Instance details

Defined in Data.Singletons.TypeLits

Methods

suppressUnusedWarnings :: () Source #

SuppressUnusedWarnings (DivModSym1 a6989586621679504167 :: TyFun Nat (Nat, Nat) -> Type) Source # 
Instance details

Defined in Data.Singletons.TypeLits

Methods

suppressUnusedWarnings :: () Source #

SuppressUnusedWarnings (QuotRemSym1 a6989586621679504161 :: TyFun Nat (Nat, Nat) -> Type) Source # 
Instance details

Defined in Data.Singletons.TypeLits

Methods

suppressUnusedWarnings :: () Source #

SuppressUnusedWarnings (FromIntegerSym0 :: TyFun Nat a6989586621679525420 -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Num

Methods

suppressUnusedWarnings :: () Source #

SuppressUnusedWarnings (ToEnumSym0 :: TyFun Nat a6989586621679763112 -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Enum

Methods

suppressUnusedWarnings :: () Source #

SuppressUnusedWarnings (DropSym0 :: TyFun Nat ([a6989586621679970156] ~> [a6989586621679970156]) -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

suppressUnusedWarnings :: () Source #

SuppressUnusedWarnings (TakeSym0 :: TyFun Nat ([a6989586621679970157] ~> [a6989586621679970157]) -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

suppressUnusedWarnings :: () Source #

SuppressUnusedWarnings (SplitAtSym0 :: TyFun Nat ([a6989586621679970155] ~> ([a6989586621679970155], [a6989586621679970155])) -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

suppressUnusedWarnings :: () Source #

SuppressUnusedWarnings (ReplicateSym0 :: TyFun Nat (a6989586621679970141 ~> [a6989586621679970141]) -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

suppressUnusedWarnings :: () Source #

SuppressUnusedWarnings (ShowsPrecSym0 :: TyFun Nat (a6989586621680290698 ~> (Symbol ~> Symbol)) -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

Methods

suppressUnusedWarnings :: () Source #

SuppressUnusedWarnings (TakeSym0 :: TyFun Nat (NonEmpty a6989586621681159612 ~> [a6989586621681159612]) -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.List.NonEmpty

Methods

suppressUnusedWarnings :: () Source #

SuppressUnusedWarnings (DropSym0 :: TyFun Nat (NonEmpty a6989586621681159611 ~> [a6989586621681159611]) -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.List.NonEmpty

Methods

suppressUnusedWarnings :: () Source #

SuppressUnusedWarnings (SplitAtSym0 :: TyFun Nat (NonEmpty a6989586621681159610 ~> ([a6989586621681159610], [a6989586621681159610])) -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.List.NonEmpty

Methods

suppressUnusedWarnings :: () Source #

SuppressUnusedWarnings (FromEnumSym0 :: TyFun a6989586621679763112 Nat -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Enum

Methods

suppressUnusedWarnings :: () Source #

SuppressUnusedWarnings (ElemIndicesSym0 :: TyFun a6989586621679970167 ([a6989586621679970167] ~> [Nat]) -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

suppressUnusedWarnings :: () Source #

SuppressUnusedWarnings (ElemIndexSym0 :: TyFun a6989586621679970168 ([a6989586621679970168] ~> Maybe Nat) -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

suppressUnusedWarnings :: () Source #

SuppressUnusedWarnings ((!!@#@$) :: TyFun (NonEmpty a6989586621681159590) (Nat ~> a6989586621681159590) -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.List.NonEmpty

Methods

suppressUnusedWarnings :: () Source #

SuppressUnusedWarnings (LengthSym0 :: TyFun (NonEmpty a6989586621681159643) Nat -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.List.NonEmpty

Methods

suppressUnusedWarnings :: () Source #

SuppressUnusedWarnings (FindIndicesSym0 :: TyFun (a6989586621679970165 ~> Bool) ([a6989586621679970165] ~> [Nat]) -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

suppressUnusedWarnings :: () Source #

SuppressUnusedWarnings (FindIndexSym0 :: TyFun (a6989586621679970166 ~> Bool) ([a6989586621679970166] ~> 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 a6989586621679974667 :: TyFun [a6989586621679970165] [Nat] -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

suppressUnusedWarnings :: () Source #

SuppressUnusedWarnings (ElemIndicesSym1 a6989586621679974701 :: TyFun [a6989586621679970167] [Nat] -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

suppressUnusedWarnings :: () Source #

SuppressUnusedWarnings (FindIndexSym1 a6989586621679974693 :: TyFun [a6989586621679970166] (Maybe Nat) -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

suppressUnusedWarnings :: () Source #

SuppressUnusedWarnings (ElemIndexSym1 a6989586621679974709 :: TyFun [a6989586621679970168] (Maybe Nat) -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

suppressUnusedWarnings :: () Source #

SuppressUnusedWarnings ((!!@#@$$) a6989586621679974286 :: TyFun Nat a6989586621679970139 -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

suppressUnusedWarnings :: () Source #

SuppressUnusedWarnings ((!!@#@$$) a6989586621681160950 :: TyFun Nat a6989586621681159590 -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.List.NonEmpty

Methods

suppressUnusedWarnings :: () Source #

SuppressUnusedWarnings (ReplicateM_Sym0 :: TyFun Nat (m6989586621681270963 a6989586621681270964 ~> m6989586621681270963 ()) -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Monad

Methods

suppressUnusedWarnings :: () Source #

SuppressUnusedWarnings (ReplicateMSym0 :: TyFun Nat (m6989586621681270965 a6989586621681270966 ~> m6989586621681270965 [a6989586621681270966]) -> 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 (t6989586621680486579 a6989586621680486595) Nat -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Foldable

Methods

suppressUnusedWarnings :: () Source #

type Demote Nat Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

type Demote Nat = Natural
type Sing Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

type Sing = SNat
type Negate (a :: Nat) Source # 
Instance details

Defined in Data.Singletons.Prelude.Num

type Negate (a :: Nat) = Error "Cannot negate a natural number" :: Nat
type Abs (a :: Nat) Source # 
Instance details

Defined in Data.Singletons.Prelude.Num

type Abs (a :: Nat) = a
type Signum (a :: Nat) Source # 
Instance details

Defined in Data.Singletons.Prelude.Num

type Signum (a :: Nat)
type FromInteger a Source # 
Instance details

Defined in Data.Singletons.Prelude.Num

type FromInteger a = a
type Succ (a :: Nat) Source # 
Instance details

Defined in Data.Singletons.Prelude.Enum

type Succ (a :: Nat)
type Pred (a :: Nat) Source # 
Instance details

Defined in Data.Singletons.Prelude.Enum

type Pred (a :: Nat)
type ToEnum a Source # 
Instance details

Defined in Data.Singletons.Prelude.Enum

type ToEnum a
type FromEnum (a :: Nat) Source # 
Instance details

Defined in Data.Singletons.Prelude.Enum

type FromEnum (a :: Nat)
type Show_ (arg0 :: Nat) Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

type Show_ (arg0 :: Nat)
type (x :: Nat) == (y :: Nat) Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

type (x :: Nat) == (y :: Nat) = DefaultEq x y
type (x :: Nat) /= (y :: Nat) Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

type (x :: Nat) /= (y :: Nat) = Not (x == y)
type Compare (a :: Nat) (b :: Nat) Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

type Compare (a :: Nat) (b :: Nat) = CmpNat a b
type (arg1 :: Nat) < (arg2 :: Nat) Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

type (arg1 :: Nat) < (arg2 :: Nat)
type (arg1 :: Nat) <= (arg2 :: Nat) Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

type (arg1 :: Nat) <= (arg2 :: Nat)
type (arg1 :: Nat) > (arg2 :: Nat) Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

type (arg1 :: Nat) > (arg2 :: Nat)
type (arg1 :: Nat) >= (arg2 :: Nat) Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

type (arg1 :: Nat) >= (arg2 :: Nat)
type Max (arg1 :: Nat) (arg2 :: Nat) Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

type Max (arg1 :: Nat) (arg2 :: Nat)
type Min (arg1 :: Nat) (arg2 :: Nat) Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

type Min (arg1 :: Nat) (arg2 :: Nat)
type (a :: Nat) + (b :: Nat) Source # 
Instance details

Defined in Data.Singletons.Prelude.Num

type (a :: Nat) + (b :: Nat) = a + b
type (a :: Nat) - (b :: Nat) Source # 
Instance details

Defined in Data.Singletons.Prelude.Num

type (a :: Nat) - (b :: Nat) = a - b
type (a :: Nat) * (b :: Nat) Source # 
Instance details

Defined in Data.Singletons.Prelude.Num

type (a :: Nat) * (b :: Nat) = a * b
type EnumFromTo (a1 :: Nat) (a2 :: Nat) Source # 
Instance details

Defined in Data.Singletons.Prelude.Enum

type EnumFromTo (a1 :: Nat) (a2 :: Nat)
type ShowList (arg1 :: [Nat]) arg2 Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

type ShowList (arg1 :: [Nat]) arg2
type Apply KnownNatSym0 (n6989586621679482027 :: Nat) Source # 
Instance details

Defined in Data.Singletons.TypeLits

type Apply KnownNatSym0 (n6989586621679482027 :: Nat) = KnownNat n6989586621679482027
type Apply Log2Sym0 (a3530822107858468865 :: Nat) Source # 
Instance details

Defined in Data.Singletons.TypeLits

type Apply Log2Sym0 (a3530822107858468865 :: Nat) = Log2 a3530822107858468865
type EnumFromThenTo (a1 :: Nat) (a2 :: Nat) (a3 :: Nat) Source # 
Instance details

Defined in Data.Singletons.Prelude.Enum

type EnumFromThenTo (a1 :: Nat) (a2 :: Nat) (a3 :: Nat)
type ShowsPrec _1 (n :: Nat) x Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

type ShowsPrec _1 (n :: Nat) x
type Apply ((<=?@#@$$) a3530822107858468865 :: TyFun Nat Bool -> Type) (b3530822107858468866 :: Nat) Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

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

Defined in Data.Singletons.TypeLits.Internal

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

Defined in Data.Singletons.TypeLits

type Apply (DivSym1 a3530822107858468865 :: TyFun Nat Nat -> Type) (b3530822107858468866 :: Nat) = Div a3530822107858468865 b3530822107858468866
type Apply (ModSym1 a3530822107858468865 :: TyFun Nat Nat -> Type) (b3530822107858468866 :: Nat) Source # 
Instance details

Defined in Data.Singletons.TypeLits

type Apply (ModSym1 a3530822107858468865 :: TyFun Nat Nat -> Type) (b3530822107858468866 :: Nat) = Mod a3530822107858468865 b3530822107858468866
type Apply (QuotSym1 a6989586621679504151 :: TyFun Nat Nat -> Type) (a6989586621679504152 :: Nat) Source # 
Instance details

Defined in Data.Singletons.TypeLits

type Apply (QuotSym1 a6989586621679504151 :: TyFun Nat Nat -> Type) (a6989586621679504152 :: Nat) = Quot a6989586621679504151 a6989586621679504152
type Apply (RemSym1 a6989586621679504141 :: TyFun Nat Nat -> Type) (a6989586621679504142 :: Nat) Source # 
Instance details

Defined in Data.Singletons.TypeLits

type Apply (RemSym1 a6989586621679504141 :: TyFun Nat Nat -> Type) (a6989586621679504142 :: Nat) = Rem a6989586621679504141 a6989586621679504142
type Apply (FromIntegerSym0 :: TyFun Nat k2 -> Type) (arg6989586621679525457 :: Nat) Source # 
Instance details

Defined in Data.Singletons.Prelude.Num

type Apply (FromIntegerSym0 :: TyFun Nat k2 -> Type) (arg6989586621679525457 :: Nat) = FromInteger arg6989586621679525457 :: k2
type Apply (ToEnumSym0 :: TyFun Nat k2 -> Type) (arg6989586621679763400 :: Nat) Source # 
Instance details

Defined in Data.Singletons.Prelude.Enum

type Apply (ToEnumSym0 :: TyFun Nat k2 -> Type) (arg6989586621679763400 :: Nat) = ToEnum arg6989586621679763400 :: k2
type Apply (FromEnumSym0 :: TyFun a Nat -> Type) (arg6989586621679763402 :: a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Enum

type Apply (FromEnumSym0 :: TyFun a Nat -> Type) (arg6989586621679763402 :: a) = FromEnum arg6989586621679763402
type Apply ((!!@#@$$) a6989586621679974286 :: TyFun Nat a -> Type) (a6989586621679974287 :: Nat) Source # 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

type Apply ((!!@#@$$) a6989586621679974286 :: TyFun Nat a -> Type) (a6989586621679974287 :: Nat) = a6989586621679974286 !! a6989586621679974287
type Apply ((!!@#@$$) a6989586621681160950 :: TyFun Nat a -> Type) (a6989586621681160951 :: Nat) Source # 
Instance details

Defined in Data.Singletons.Prelude.List.NonEmpty

type Apply ((!!@#@$$) a6989586621681160950 :: TyFun Nat a -> Type) (a6989586621681160951 :: Nat) = a6989586621681160950 !! a6989586621681160951
type Apply (<=?@#@$) (a3530822107858468865 :: Nat) Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

type Apply (<=?@#@$) (a3530822107858468865 :: Nat) = (<=?@#@$$) a3530822107858468865
type Apply (^@#@$) (a3530822107858468865 :: Nat) Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

type Apply (^@#@$) (a3530822107858468865 :: Nat) = (^@#@$$) a3530822107858468865
type Apply DivSym0 (a3530822107858468865 :: Nat) Source # 
Instance details

Defined in Data.Singletons.TypeLits

type Apply DivSym0 (a3530822107858468865 :: Nat) = DivSym1 a3530822107858468865
type Apply ModSym0 (a3530822107858468865 :: Nat) Source # 
Instance details

Defined in Data.Singletons.TypeLits

type Apply ModSym0 (a3530822107858468865 :: Nat) = ModSym1 a3530822107858468865
type Apply QuotSym0 (a6989586621679504151 :: Nat) Source # 
Instance details

Defined in Data.Singletons.TypeLits

type Apply QuotSym0 (a6989586621679504151 :: Nat) = QuotSym1 a6989586621679504151
type Apply RemSym0 (a6989586621679504141 :: Nat) Source # 
Instance details

Defined in Data.Singletons.TypeLits

type Apply RemSym0 (a6989586621679504141 :: Nat) = RemSym1 a6989586621679504141
type Apply DivModSym0 (a6989586621679504167 :: Nat) Source # 
Instance details

Defined in Data.Singletons.TypeLits

type Apply DivModSym0 (a6989586621679504167 :: Nat) = DivModSym1 a6989586621679504167
type Apply QuotRemSym0 (a6989586621679504161 :: Nat) Source # 
Instance details

Defined in Data.Singletons.TypeLits

type Apply QuotRemSym0 (a6989586621679504161 :: Nat) = QuotRemSym1 a6989586621679504161
type Apply (DivModSym1 a6989586621679504167 :: TyFun Nat (Nat, Nat) -> Type) (a6989586621679504168 :: Nat) Source # 
Instance details

Defined in Data.Singletons.TypeLits

type Apply (DivModSym1 a6989586621679504167 :: TyFun Nat (Nat, Nat) -> Type) (a6989586621679504168 :: Nat) = DivMod a6989586621679504167 a6989586621679504168
type Apply (QuotRemSym1 a6989586621679504161 :: TyFun Nat (Nat, Nat) -> Type) (a6989586621679504162 :: Nat) Source # 
Instance details

Defined in Data.Singletons.TypeLits

type Apply (QuotRemSym1 a6989586621679504161 :: TyFun Nat (Nat, Nat) -> Type) (a6989586621679504162 :: Nat) = QuotRem a6989586621679504161 a6989586621679504162
type Apply (DropSym0 :: TyFun Nat ([a6989586621679970156] ~> [a6989586621679970156]) -> Type) (a6989586621679974453 :: Nat) Source # 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

type Apply (DropSym0 :: TyFun Nat ([a6989586621679970156] ~> [a6989586621679970156]) -> Type) (a6989586621679974453 :: Nat) = DropSym1 a6989586621679974453 a6989586621679970156 :: TyFun [a6989586621679970156] [a6989586621679970156] -> Type
type Apply (TakeSym0 :: TyFun Nat ([a6989586621679970157] ~> [a6989586621679970157]) -> Type) (a6989586621679974467 :: Nat) Source # 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

type Apply (TakeSym0 :: TyFun Nat ([a6989586621679970157] ~> [a6989586621679970157]) -> Type) (a6989586621679974467 :: Nat) = TakeSym1 a6989586621679974467 a6989586621679970157 :: TyFun [a6989586621679970157] [a6989586621679970157] -> Type
type Apply (SplitAtSym0 :: TyFun Nat ([a6989586621679970155] ~> ([a6989586621679970155], [a6989586621679970155])) -> Type) (a6989586621679974447 :: Nat) Source # 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

type Apply (SplitAtSym0 :: TyFun Nat ([a6989586621679970155] ~> ([a6989586621679970155], [a6989586621679970155])) -> Type) (a6989586621679974447 :: Nat) = SplitAtSym1 a6989586621679974447 a6989586621679970155 :: TyFun [a6989586621679970155] ([a6989586621679970155], [a6989586621679970155]) -> Type
type Apply (ReplicateSym0 :: TyFun Nat (a6989586621679970141 ~> [a6989586621679970141]) -> Type) (a6989586621679974306 :: Nat) Source # 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

type Apply (ReplicateSym0 :: TyFun Nat (a6989586621679970141 ~> [a6989586621679970141]) -> Type) (a6989586621679974306 :: Nat) = ReplicateSym1 a6989586621679974306 a6989586621679970141 :: TyFun a6989586621679970141 [a6989586621679970141] -> Type
type Apply (ShowsPrecSym0 :: TyFun Nat (a6989586621680290698 ~> (Symbol ~> Symbol)) -> Type) (arg6989586621680291136 :: Nat) Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

type Apply (ShowsPrecSym0 :: TyFun Nat (a6989586621680290698 ~> (Symbol ~> Symbol)) -> Type) (arg6989586621680291136 :: Nat) = ShowsPrecSym1 arg6989586621680291136 a6989586621680290698 :: TyFun a6989586621680290698 (Symbol ~> Symbol) -> Type
type Apply (TakeSym0 :: TyFun Nat (NonEmpty a6989586621681159612 ~> [a6989586621681159612]) -> Type) (a6989586621681161161 :: Nat) Source # 
Instance details

Defined in Data.Singletons.Prelude.List.NonEmpty

type Apply (TakeSym0 :: TyFun Nat (NonEmpty a6989586621681159612 ~> [a6989586621681159612]) -> Type) (a6989586621681161161 :: Nat) = TakeSym1 a6989586621681161161 a6989586621681159612 :: TyFun (NonEmpty a6989586621681159612) [a6989586621681159612] -> Type
type Apply (DropSym0 :: TyFun Nat (NonEmpty a6989586621681159611 ~> [a6989586621681159611]) -> Type) (a6989586621681161153 :: Nat) Source # 
Instance details

Defined in Data.Singletons.Prelude.List.NonEmpty

type Apply (DropSym0 :: TyFun Nat (NonEmpty a6989586621681159611 ~> [a6989586621681159611]) -> Type) (a6989586621681161153 :: Nat) = DropSym1 a6989586621681161153 a6989586621681159611 :: TyFun (NonEmpty a6989586621681159611) [a6989586621681159611] -> Type
type Apply (SplitAtSym0 :: TyFun Nat (NonEmpty a6989586621681159610 ~> ([a6989586621681159610], [a6989586621681159610])) -> Type) (a6989586621681161145 :: Nat) Source # 
Instance details

Defined in Data.Singletons.Prelude.List.NonEmpty

type Apply (SplitAtSym0 :: TyFun Nat (NonEmpty a6989586621681159610 ~> ([a6989586621681159610], [a6989586621681159610])) -> Type) (a6989586621681161145 :: Nat) = SplitAtSym1 a6989586621681161145 a6989586621681159610 :: TyFun (NonEmpty a6989586621681159610) ([a6989586621681159610], [a6989586621681159610]) -> Type
type Apply (ElemIndicesSym0 :: TyFun a6989586621679970167 ([a6989586621679970167] ~> [Nat]) -> Type) (a6989586621679974701 :: a6989586621679970167) Source # 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

type Apply (ElemIndicesSym0 :: TyFun a6989586621679970167 ([a6989586621679970167] ~> [Nat]) -> Type) (a6989586621679974701 :: a6989586621679970167) = ElemIndicesSym1 a6989586621679974701
type Apply (ElemIndexSym0 :: TyFun a6989586621679970168 ([a6989586621679970168] ~> Maybe Nat) -> Type) (a6989586621679974709 :: a6989586621679970168) Source # 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

type Apply (ElemIndexSym0 :: TyFun a6989586621679970168 ([a6989586621679970168] ~> Maybe Nat) -> Type) (a6989586621679974709 :: a6989586621679970168) = ElemIndexSym1 a6989586621679974709
type Apply (ReplicateM_Sym0 :: TyFun Nat (m6989586621681270963 a6989586621681270964 ~> m6989586621681270963 ()) -> Type) (a6989586621681271323 :: Nat) Source # 
Instance details

Defined in Data.Singletons.Prelude.Monad

type Apply (ReplicateM_Sym0 :: TyFun Nat (m6989586621681270963 a6989586621681270964 ~> m6989586621681270963 ()) -> Type) (a6989586621681271323 :: Nat) = ReplicateM_Sym1 a6989586621681271323 m6989586621681270963 a6989586621681270964 :: TyFun (m6989586621681270963 a6989586621681270964) (m6989586621681270963 ()) -> Type
type Apply (ReplicateMSym0 :: TyFun Nat (m6989586621681270965 a6989586621681270966 ~> m6989586621681270965 [a6989586621681270966]) -> Type) (a6989586621681271342 :: Nat) Source # 
Instance details

Defined in Data.Singletons.Prelude.Monad

type Apply (ReplicateMSym0 :: TyFun Nat (m6989586621681270965 a6989586621681270966 ~> m6989586621681270965 [a6989586621681270966]) -> Type) (a6989586621681271342 :: Nat) = ReplicateMSym1 a6989586621681271342 m6989586621681270965 a6989586621681270966 :: TyFun (m6989586621681270965 a6989586621681270966) (m6989586621681270965 [a6989586621681270966]) -> Type
type Apply (LengthSym0 :: TyFun (NonEmpty a) Nat -> Type) (a6989586621681161362 :: NonEmpty a) Source # 
Instance details

Defined in Data.Singletons.Prelude.List.NonEmpty

type Apply (LengthSym0 :: TyFun (NonEmpty a) Nat -> Type) (a6989586621681161362 :: NonEmpty a) = Length a6989586621681161362
type Apply (LengthSym0 :: TyFun (t a) Nat -> Type) (arg6989586621680487240 :: t a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Foldable

type Apply (LengthSym0 :: TyFun (t a) Nat -> Type) (arg6989586621680487240 :: t a) = Length arg6989586621680487240
type Apply (FindIndicesSym1 a6989586621679974667 :: TyFun [a] [Nat] -> Type) (a6989586621679974668 :: [a]) Source # 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

type Apply (FindIndicesSym1 a6989586621679974667 :: TyFun [a] [Nat] -> Type) (a6989586621679974668 :: [a]) = FindIndices a6989586621679974667 a6989586621679974668
type Apply (ElemIndicesSym1 a6989586621679974701 :: TyFun [a] [Nat] -> Type) (a6989586621679974702 :: [a]) Source # 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

type Apply (ElemIndicesSym1 a6989586621679974701 :: TyFun [a] [Nat] -> Type) (a6989586621679974702 :: [a]) = ElemIndices a6989586621679974701 a6989586621679974702
type Apply (FindIndexSym1 a6989586621679974693 :: TyFun [a] (Maybe Nat) -> Type) (a6989586621679974694 :: [a]) Source # 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

type Apply (FindIndexSym1 a6989586621679974693 :: TyFun [a] (Maybe Nat) -> Type) (a6989586621679974694 :: [a]) = FindIndex a6989586621679974693 a6989586621679974694
type Apply (ElemIndexSym1 a6989586621679974709 :: TyFun [a] (Maybe Nat) -> Type) (a6989586621679974710 :: [a]) Source # 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

type Apply (ElemIndexSym1 a6989586621679974709 :: TyFun [a] (Maybe Nat) -> Type) (a6989586621679974710 :: [a]) = ElemIndex a6989586621679974709 a6989586621679974710
type Apply ((!!@#@$) :: TyFun [a6989586621679970139] (Nat ~> a6989586621679970139) -> Type) (a6989586621679974286 :: [a6989586621679970139]) Source # 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

type Apply ((!!@#@$) :: TyFun [a6989586621679970139] (Nat ~> a6989586621679970139) -> Type) (a6989586621679974286 :: [a6989586621679970139]) = (!!@#@$$) a6989586621679974286
type Apply ((!!@#@$) :: TyFun (NonEmpty a6989586621681159590) (Nat ~> a6989586621681159590) -> Type) (a6989586621681160950 :: NonEmpty a6989586621681159590) Source # 
Instance details

Defined in Data.Singletons.Prelude.List.NonEmpty

type Apply ((!!@#@$) :: TyFun (NonEmpty a6989586621681159590) (Nat ~> a6989586621681159590) -> Type) (a6989586621681160950 :: NonEmpty a6989586621681159590) = (!!@#@$$) a6989586621681160950
type Apply (FindIndicesSym0 :: TyFun (a6989586621679970165 ~> Bool) ([a6989586621679970165] ~> [Nat]) -> Type) (a6989586621679974667 :: a6989586621679970165 ~> Bool) Source # 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

type Apply (FindIndicesSym0 :: TyFun (a6989586621679970165 ~> Bool) ([a6989586621679970165] ~> [Nat]) -> Type) (a6989586621679974667 :: a6989586621679970165 ~> Bool) = FindIndicesSym1 a6989586621679974667
type Apply (FindIndexSym0 :: TyFun (a6989586621679970166 ~> Bool) ([a6989586621679970166] ~> Maybe Nat) -> Type) (a6989586621679974693 :: a6989586621679970166 ~> Bool) Source # 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

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

data Symbol #

Instances

Instances details
Eq Symbol

This bogus instance is helpful for people who want to define functions over Symbols that will only be used at the type level or as singletons.

Instance details

Defined in Data.Singletons.TypeLits

Methods

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

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

Ord Symbol 
Instance details

Defined in Data.Singletons.TypeLits

Methods

compare :: Symbol -> Symbol -> Ordering

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

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

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

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

max :: Symbol -> Symbol -> Symbol

min :: Symbol -> Symbol -> Symbol

Show Symbol 
Instance details

Defined in Data.Singletons.TypeLits

Methods

showsPrec :: Int -> Symbol -> ShowS

show :: Symbol -> String

showList :: [Symbol] -> ShowS

IsString Symbol 
Instance details

Defined in Data.Singletons.TypeLits

Methods

fromString :: String -> Symbol

Semigroup Symbol 
Instance details

Defined in Data.Singletons.TypeLits

Methods

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

sconcat :: NonEmpty Symbol -> Symbol

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

Monoid Symbol 
Instance details

Defined in Data.Singletons.TypeLits

Methods

mempty :: Symbol

mappend :: Symbol -> Symbol -> Symbol

mconcat :: [Symbol] -> Symbol

SingKind Symbol Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

Associated Types

type Demote Symbol = (r :: Type) Source #

Methods

fromSing :: forall (a :: Symbol). Sing a -> Demote Symbol Source #

toSing :: Demote Symbol -> SomeSing Symbol Source #

SingKind PErrorMessage Source # 
Instance details

Defined in Data.Singletons.TypeError

Associated Types

type Demote PErrorMessage = (r :: Type) Source #

Methods

fromSing :: forall (a :: PErrorMessage). Sing a -> Demote PErrorMessage Source #

toSing :: Demote PErrorMessage -> SomeSing PErrorMessage Source #

SingKind Symbol 
Instance details

Defined in GHC.Generics

Associated Types

type DemoteRep Symbol

Methods

fromSing :: forall (a :: Symbol). Sing a -> DemoteRep Symbol

SDecide Symbol Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

Methods

(%~) :: forall (a :: Symbol) (b :: Symbol). Sing a -> Sing b -> Decision (a :~: b) Source #

PEq Symbol Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

Associated Types

type x == y :: Bool Source #

type x /= y :: Bool Source #

SEq Symbol Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

Methods

(%==) :: forall (a :: Symbol) (b :: Symbol). Sing a -> Sing b -> Sing (a == b) Source #

(%/=) :: forall (a :: Symbol) (b :: Symbol). Sing a -> Sing b -> Sing (a /= b) Source #

SOrd Symbol Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

Methods

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

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

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

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

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

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

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

POrd Symbol Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

Associated Types

type Compare arg arg :: Ordering Source #

type arg < arg :: Bool Source #

type arg <= arg :: Bool Source #

type arg > arg :: Bool Source #

type arg >= arg :: Bool Source #

type Max arg arg :: a Source #

type Min arg arg :: a Source #

SSemigroup Symbol Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

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

sSconcat :: forall (t :: NonEmpty Symbol). Sing t -> Sing (Apply SconcatSym0 t) Source #

PSemigroup Symbol Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

Associated Types

type arg <> arg :: a Source #

type Sconcat arg :: a Source #

SShow Symbol Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

Methods

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

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

sShowList :: forall (t :: [Symbol]) (t :: Symbol). Sing t -> Sing t -> Sing (Apply (Apply ShowListSym0 t) t) Source #

PShow Symbol Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

Associated Types

type ShowsPrec arg arg arg :: Symbol Source #

type Show_ arg :: Symbol Source #

type ShowList arg arg :: Symbol Source #

SMonoid Symbol Source # 
Instance details

Defined in Data.Singletons.Prelude.Monoid

Methods

sMempty :: Sing MemptySym0 Source #

sMappend :: forall (t :: Symbol) (t :: Symbol). Sing t -> Sing t -> Sing (Apply (Apply MappendSym0 t) t) Source #

sMconcat :: forall (t :: [Symbol]). Sing t -> Sing (Apply MconcatSym0 t) Source #

PMonoid Symbol Source # 
Instance details

Defined in Data.Singletons.Prelude.Monoid

Associated Types

type Mempty :: a Source #

type Mappend arg arg :: a Source #

type Mconcat arg :: a Source #

SIsString Symbol Source # 
Instance details

Defined in Data.Singletons.Prelude.IsString

Methods

sFromString :: forall (t :: Symbol). Sing t -> Sing (Apply FromStringSym0 t) Source #

PIsString Symbol Source # 
Instance details

Defined in Data.Singletons.Prelude.IsString

Associated Types

type FromString arg :: a Source #

KnownSymbol n => SingI (n :: Symbol) Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

Methods

sing :: Sing n Source #

KnownSymbol a => SingI (a :: Symbol) 
Instance details

Defined in GHC.Generics

Methods

sing :: Sing a

SingI t => SingI ('Text t :: ErrorMessage' Symbol) Source # 
Instance details

Defined in Data.Singletons.TypeError

Methods

sing :: Sing ('Text t) Source #

SingI ty => SingI ('ShowType ty :: ErrorMessage' Symbol) Source # 
Instance details

Defined in Data.Singletons.TypeError

Methods

sing :: Sing ('ShowType ty) Source #

(SingI e1, SingI e2) => SingI (e1 :<>: e2 :: ErrorMessage' Symbol) Source # 
Instance details

Defined in Data.Singletons.TypeError

Methods

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

(SingI e1, SingI e2) => SingI (e1 :$$: e2 :: ErrorMessage' Symbol) Source # 
Instance details

Defined in Data.Singletons.TypeError

Methods

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

SingI ShowParenSym0 Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing ShowParenSym0 Source #

SingI UnlinesSym0 Source # 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing UnlinesSym0 Source #

SingI UnwordsSym0 Source # 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing UnwordsSym0 Source #

SingI ShowSpaceSym0 Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing ShowSpaceSym0 Source #

SingI ShowCommaSpaceSym0 Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing ShowCommaSpaceSym0 Source #

SingI ShowCharSym0 Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing ShowCharSym0 Source #

SingI ShowStringSym0 Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing ShowStringSym0 Source #

SuppressUnusedWarnings ShowParenSym0 Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

Methods

suppressUnusedWarnings :: () Source #

SuppressUnusedWarnings UnlinesSym0 Source # 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

suppressUnusedWarnings :: () Source #

SuppressUnusedWarnings UnwordsSym0 Source # 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

suppressUnusedWarnings :: () Source #

SuppressUnusedWarnings KnownSymbolSym0 Source # 
Instance details

Defined in Data.Singletons.TypeLits

Methods

suppressUnusedWarnings :: () Source #

SuppressUnusedWarnings ShowSpaceSym0 Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

Methods

suppressUnusedWarnings :: () Source #

SuppressUnusedWarnings ShowCommaSpaceSym0 Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

Methods

suppressUnusedWarnings :: () Source #

SuppressUnusedWarnings ShowCharSym0 Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

Methods

suppressUnusedWarnings :: () Source #

SuppressUnusedWarnings ShowStringSym0 Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

Methods

suppressUnusedWarnings :: () Source #

SingI (TypeErrorSym0 :: TyFun PErrorMessage b6989586621681327314 -> 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 [a6989586621680290698] (Symbol ~> Symbol) -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

Methods

suppressUnusedWarnings :: () Source #

SuppressUnusedWarnings (ShowsPrecSym0 :: TyFun Nat (a6989586621680290698 ~> (Symbol ~> Symbol)) -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

Methods

suppressUnusedWarnings :: () Source #

SuppressUnusedWarnings (ShowCharSym1 a6989586621680291102 :: TyFun Symbol Symbol -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

Methods

suppressUnusedWarnings :: () Source #

SuppressUnusedWarnings (ShowStringSym1 a6989586621680291092 :: TyFun Symbol Symbol -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

Methods

suppressUnusedWarnings :: () Source #

SuppressUnusedWarnings (FromStringSym0 :: TyFun Symbol a6989586621681259476 -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.IsString

Methods

suppressUnusedWarnings :: () Source #

SuppressUnusedWarnings (Show_Sym0 :: TyFun a6989586621680290698 Symbol -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

Methods

suppressUnusedWarnings :: () Source #

SuppressUnusedWarnings (ShowsSym0 :: TyFun a6989586621680290683 (Symbol ~> Symbol) -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

Methods

suppressUnusedWarnings :: () Source #

SuppressUnusedWarnings (ShowParenSym1 a6989586621680291074 :: TyFun (Symbol ~> Symbol) (Symbol ~> Symbol) -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

Methods

suppressUnusedWarnings :: () Source #

SuppressUnusedWarnings (ShowListWithSym0 :: TyFun (a6989586621680290682 ~> (Symbol ~> Symbol)) ([a6989586621680290682] ~> (Symbol ~> Symbol)) -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

Methods

suppressUnusedWarnings :: () Source #

SuppressUnusedWarnings (TypeErrorSym0 :: TyFun PErrorMessage b6989586621681327314 -> Type) Source # 
Instance details

Defined in Data.Singletons.TypeError

Methods

suppressUnusedWarnings :: () Source #

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

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing (ShowListWithSym1 d) Source #

(SShow a, SingI d) => SingI (ShowListSym1 d :: TyFun Symbol Symbol -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing (ShowListSym1 d) Source #

(SShow a, SingI d) => SingI (ShowsSym1 d :: TyFun Symbol Symbol -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing (ShowsSym1 d) Source #

(SingI d1, SingI d2) => SingI (ShowParenSym2 d1 d2 :: TyFun Symbol Symbol -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing (ShowParenSym2 d1 d2) Source #

SingI (ErrorSym0 :: TyFun Symbol a -> Type) Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

Methods

sing :: Sing ErrorSym0 Source #

SingI (ErrorWithoutStackTraceSym0 :: TyFun Symbol a -> Type) Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

Methods

sing :: Sing ErrorWithoutStackTraceSym0 Source #

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

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing (ShowsPrecSym1 d a) Source #

SingI (ShowTypeSym0 :: TyFun t (ErrorMessage' Symbol) -> Type) Source # 
Instance details

Defined in Data.Singletons.TypeError

Methods

sing :: Sing ShowTypeSym0 Source #

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

Defined in Data.Singletons.TypeError

Methods

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

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

Defined in Data.Singletons.TypeError

Methods

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

SuppressUnusedWarnings (ShowListWithSym1 a6989586621680291108 :: TyFun [a6989586621680290682] (Symbol ~> Symbol) -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

Methods

suppressUnusedWarnings :: () Source #

SuppressUnusedWarnings (ShowListSym1 arg6989586621680291144 :: TyFun Symbol Symbol -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

Methods

suppressUnusedWarnings :: () Source #

SuppressUnusedWarnings (ShowsSym1 a6989586621680291128 :: TyFun Symbol Symbol -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

Methods

suppressUnusedWarnings :: () Source #

SuppressUnusedWarnings (ShowParenSym2 a6989586621680291075 a6989586621680291074 :: TyFun Symbol Symbol -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

Methods

suppressUnusedWarnings :: () Source #

SuppressUnusedWarnings (ShowsPrecSym1 arg6989586621680291136 a6989586621680290698 :: TyFun a6989586621680290698 (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 arg6989586621680291137 arg6989586621680291136 :: TyFun Symbol Symbol -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

Methods

suppressUnusedWarnings :: () Source #

SuppressUnusedWarnings (ShowListWithSym2 a6989586621680291109 a6989586621680291108 :: TyFun Symbol Symbol -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

Methods

suppressUnusedWarnings :: () Source #

type Demote Symbol Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

type Demote Symbol = Text
type Demote PErrorMessage Source # 
Instance details

Defined in Data.Singletons.TypeError

type Demote PErrorMessage = ErrorMessage
type Sing Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

type Sing = SSymbol
type Sing Source # 
Instance details

Defined in Data.Singletons.TypeError

type Sing = SErrorMessage
type DemoteRep Symbol 
Instance details

Defined in GHC.Generics

type DemoteRep Symbol = String
data Sing (s :: Symbol) 
Instance details

Defined in GHC.Generics

data Sing (s :: Symbol) where
type Mempty Source # 
Instance details

Defined in Data.Singletons.Prelude.Monoid

type Mempty
type Sconcat (arg0 :: NonEmpty Symbol) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

type Sconcat (arg0 :: NonEmpty Symbol)
type Show_ (arg0 :: Symbol) Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

type Show_ (arg0 :: Symbol)
type Mconcat (arg0 :: [Symbol]) Source # 
Instance details

Defined in Data.Singletons.Prelude.Monoid

type Mconcat (arg0 :: [Symbol])
type FromString a Source # 
Instance details

Defined in Data.Singletons.Prelude.IsString

type FromString a = a
type (x :: Symbol) == (y :: Symbol) Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

type (x :: Symbol) == (y :: Symbol) = DefaultEq x y
type (x :: Symbol) /= (y :: Symbol) Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

type (x :: Symbol) /= (y :: Symbol) = Not (x == y)
type Compare (a :: Symbol) (b :: Symbol) Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

type Compare (a :: Symbol) (b :: Symbol) = CmpSymbol a b
type (arg1 :: Symbol) < (arg2 :: Symbol) Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

type (arg1 :: Symbol) < (arg2 :: Symbol)
type (arg1 :: Symbol) <= (arg2 :: Symbol) Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

type (arg1 :: Symbol) <= (arg2 :: Symbol)
type (arg1 :: Symbol) > (arg2 :: Symbol) Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

type (arg1 :: Symbol) > (arg2 :: Symbol)
type (arg1 :: Symbol) >= (arg2 :: Symbol) Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

type (arg1 :: Symbol) >= (arg2 :: Symbol)
type Max (arg1 :: Symbol) (arg2 :: Symbol) Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

type Max (arg1 :: Symbol) (arg2 :: Symbol)
type Min (arg1 :: Symbol) (arg2 :: Symbol) Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

type Min (arg1 :: Symbol) (arg2 :: Symbol)
type (a :: Symbol) <> (b :: Symbol) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

type (a :: Symbol) <> (b :: Symbol) = AppendSymbol a b
type ShowList (arg1 :: [Symbol]) arg2 Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

type ShowList (arg1 :: [Symbol]) arg2
type Mappend (arg1 :: Symbol) (arg2 :: Symbol) Source # 
Instance details

Defined in Data.Singletons.Prelude.Monoid

type Mappend (arg1 :: Symbol) (arg2 :: Symbol)
type Apply KnownSymbolSym0 (n6989586621679482093 :: Symbol) Source # 
Instance details

Defined in Data.Singletons.TypeLits

type Apply KnownSymbolSym0 (n6989586621679482093 :: Symbol) = KnownSymbol n6989586621679482093
type Apply ShowSpaceSym0 (a6989586621680291065 :: Symbol) Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

type Apply ShowSpaceSym0 (a6989586621680291065 :: Symbol) = ShowSpace a6989586621680291065
type Apply ShowCommaSpaceSym0 (a6989586621680291060 :: Symbol) Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

type Apply ShowCommaSpaceSym0 (a6989586621680291060 :: Symbol) = ShowCommaSpace a6989586621680291060
type ShowsPrec a1 (a2 :: Symbol) a3 Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

type ShowsPrec a1 (a2 :: Symbol) a3
type Apply (ShowCharSym1 a6989586621680291102 :: TyFun Symbol Symbol -> Type) (a6989586621680291103 :: Symbol) Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

type Apply (ShowCharSym1 a6989586621680291102 :: TyFun Symbol Symbol -> Type) (a6989586621680291103 :: Symbol) = ShowChar a6989586621680291102 a6989586621680291103
type Apply (ShowStringSym1 a6989586621680291092 :: TyFun Symbol Symbol -> Type) (a6989586621680291093 :: Symbol) Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

type Apply (ShowStringSym1 a6989586621680291092 :: TyFun Symbol Symbol -> Type) (a6989586621680291093 :: Symbol) = ShowString a6989586621680291092 a6989586621680291093
type Apply (FromStringSym0 :: TyFun Symbol k2 -> Type) (arg6989586621681259502 :: Symbol) Source # 
Instance details

Defined in Data.Singletons.Prelude.IsString

type Apply (FromStringSym0 :: TyFun Symbol k2 -> Type) (arg6989586621681259502 :: Symbol) = FromString arg6989586621681259502 :: k2
type Apply (Show_Sym0 :: TyFun a Symbol -> Type) (arg6989586621680291142 :: a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

type Apply (Show_Sym0 :: TyFun a Symbol -> Type) (arg6989586621680291142 :: a) = Show_ arg6989586621680291142
type Apply (TypeErrorSym0 :: TyFun PErrorMessage k2 -> Type) (a6989586621681327315 :: PErrorMessage) Source # 
Instance details

Defined in Data.Singletons.TypeError

type Apply (TypeErrorSym0 :: TyFun PErrorMessage k2 -> Type) (a6989586621681327315 :: PErrorMessage) = TypeError a6989586621681327315 :: k2
type Apply (ShowListSym1 arg6989586621680291144 :: TyFun Symbol Symbol -> Type) (arg6989586621680291145 :: Symbol) Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

type Apply (ShowListSym1 arg6989586621680291144 :: TyFun Symbol Symbol -> Type) (arg6989586621680291145 :: Symbol) = ShowList arg6989586621680291144 arg6989586621680291145
type Apply (ShowsSym1 a6989586621680291128 :: TyFun Symbol Symbol -> Type) (a6989586621680291129 :: Symbol) Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

type Apply (ShowsSym1 a6989586621680291128 :: TyFun Symbol Symbol -> Type) (a6989586621680291129 :: Symbol) = Shows a6989586621680291128 a6989586621680291129
type Apply (ShowParenSym2 a6989586621680291075 a6989586621680291074 :: TyFun Symbol Symbol -> Type) (a6989586621680291076 :: Symbol) Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

type Apply (ShowParenSym2 a6989586621680291075 a6989586621680291074 :: TyFun Symbol Symbol -> Type) (a6989586621680291076 :: Symbol) = ShowParen a6989586621680291075 a6989586621680291074 a6989586621680291076
type Apply (ShowsPrecSym2 arg6989586621680291137 arg6989586621680291136 :: TyFun Symbol Symbol -> Type) (arg6989586621680291138 :: Symbol) Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

type Apply (ShowsPrecSym2 arg6989586621680291137 arg6989586621680291136 :: TyFun Symbol Symbol -> Type) (arg6989586621680291138 :: Symbol) = ShowsPrec arg6989586621680291137 arg6989586621680291136 arg6989586621680291138
type Apply (ShowListWithSym2 a6989586621680291109 a6989586621680291108 :: TyFun Symbol Symbol -> Type) (a6989586621680291110 :: Symbol) Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

type Apply (ShowListWithSym2 a6989586621680291109 a6989586621680291108 :: TyFun Symbol Symbol -> Type) (a6989586621680291110 :: Symbol) = ShowListWith a6989586621680291109 a6989586621680291108 a6989586621680291110
type Apply ShowParenSym0 (a6989586621680291074 :: Bool) Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

type Apply ShowParenSym0 (a6989586621680291074 :: Bool) = ShowParenSym1 a6989586621680291074
type Apply ShowCharSym0 (a6989586621680291102 :: Symbol) Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

type Apply ShowCharSym0 (a6989586621680291102 :: Symbol) = ShowCharSym1 a6989586621680291102
type Apply ShowStringSym0 (a6989586621680291092 :: Symbol) Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

type Apply ShowStringSym0 (a6989586621680291092 :: Symbol) = ShowStringSym1 a6989586621680291092
type Apply (ShowsPrecSym0 :: TyFun Nat (a6989586621680290698 ~> (Symbol ~> Symbol)) -> Type) (arg6989586621680291136 :: Nat) Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

type Apply (ShowsPrecSym0 :: TyFun Nat (a6989586621680290698 ~> (Symbol ~> Symbol)) -> Type) (arg6989586621680291136 :: Nat) = ShowsPrecSym1 arg6989586621680291136 a6989586621680290698 :: TyFun a6989586621680290698 (Symbol ~> Symbol) -> Type
type Apply (ShowsSym0 :: TyFun a6989586621680290683 (Symbol ~> Symbol) -> Type) (a6989586621680291128 :: a6989586621680290683) Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

type Apply (ShowsSym0 :: TyFun a6989586621680290683 (Symbol ~> Symbol) -> Type) (a6989586621680291128 :: a6989586621680290683) = ShowsSym1 a6989586621680291128
type Apply (ShowsPrecSym1 arg6989586621680291136 a6989586621680290698 :: TyFun a6989586621680290698 (Symbol ~> Symbol) -> Type) (arg6989586621680291137 :: a6989586621680290698) Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

type Apply (ShowsPrecSym1 arg6989586621680291136 a6989586621680290698 :: TyFun a6989586621680290698 (Symbol ~> Symbol) -> Type) (arg6989586621680291137 :: a6989586621680290698) = ShowsPrecSym2 arg6989586621680291136 arg6989586621680291137
type Apply UnlinesSym0 (a6989586621679974894 :: [Symbol]) Source # 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

type Apply UnlinesSym0 (a6989586621679974894 :: [Symbol]) = Unlines a6989586621679974894
type Apply UnwordsSym0 (a6989586621679974883 :: [Symbol]) Source # 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

type Apply UnwordsSym0 (a6989586621679974883 :: [Symbol]) = Unwords a6989586621679974883
type Apply (ShowListSym0 :: TyFun [a6989586621680290698] (Symbol ~> Symbol) -> Type) (arg6989586621680291144 :: [a6989586621680290698]) Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

type Apply (ShowListSym0 :: TyFun [a6989586621680290698] (Symbol ~> Symbol) -> Type) (arg6989586621680291144 :: [a6989586621680290698]) = ShowListSym1 arg6989586621680291144
type Apply (ShowListWithSym1 a6989586621680291108 :: TyFun [a6989586621680290682] (Symbol ~> Symbol) -> Type) (a6989586621680291109 :: [a6989586621680290682]) Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

type Apply (ShowListWithSym1 a6989586621680291108 :: TyFun [a6989586621680290682] (Symbol ~> Symbol) -> Type) (a6989586621680291109 :: [a6989586621680290682]) = ShowListWithSym2 a6989586621680291108 a6989586621680291109
type Apply (ShowParenSym1 a6989586621680291074 :: TyFun (Symbol ~> Symbol) (Symbol ~> Symbol) -> Type) (a6989586621680291075 :: Symbol ~> Symbol) Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

type Apply (ShowParenSym1 a6989586621680291074 :: TyFun (Symbol ~> Symbol) (Symbol ~> Symbol) -> Type) (a6989586621680291075 :: Symbol ~> Symbol) = ShowParenSym2 a6989586621680291074 a6989586621680291075
type Apply (ShowListWithSym0 :: TyFun (a6989586621680290682 ~> (Symbol ~> Symbol)) ([a6989586621680290682] ~> (Symbol ~> Symbol)) -> Type) (a6989586621680291108 :: a6989586621680290682 ~> (Symbol ~> Symbol)) Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

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

type family Sing :: k -> Type Source #

The singleton kind-indexed type family.

Instances

Instances details
type Sing Source # 
Instance details

Defined in Data.Singletons.Prelude.Instances

type Sing = SBool
type Sing Source # 
Instance details

Defined in Data.Singletons.Prelude.Instances

type Sing = SOrdering
type Sing Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

type Sing = SNat
type Sing Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

type Sing = SSymbol
type Sing Source # 
Instance details

Defined in Data.Singletons.Prelude.Instances

type Sing = STuple0
type Sing Source # 
Instance details

Defined in Data.Singletons.Prelude.Instances

type Sing = SVoid
type Sing Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

type Sing = SAll
type Sing Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

type Sing = SAny
type Sing Source # 
Instance details

Defined in Data.Singletons.TypeError

type Sing = SErrorMessage
type Sing Source # 
Instance details

Defined in Data.Singletons.Prelude.Instances

type Sing = SList :: [a] -> Type
type Sing Source # 
Instance details

Defined in Data.Singletons.Prelude.Instances

type Sing = SMaybe :: Maybe a -> Type
type Sing Source #

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

Conceivably, one could generalize this instance to `Sing @k` for any kind k, and remove all other Sing instances. We don't adopt this design, however, since it is far more convenient in practice to work with explicit singleton values than TypeReps (for instance, TypeReps are more difficult to pattern match on, and require extra runtime checks).

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

Instance details

Defined in Data.Singletons.TypeRepTYPE

type Sing = TypeRep :: TYPE rep -> Type
type Sing Source # 
Instance details

Defined in Data.Singletons.Prelude.Instances

type Sing = SNonEmpty :: NonEmpty a -> Type
type Sing Source # 
Instance details

Defined in Data.Singletons.Prelude.Ord

type Sing = SDown :: Down a -> Type
type Sing Source # 
Instance details

Defined in Data.Singletons.Prelude.Instances

type Sing = SIdentity :: Identity a -> Type
type Sing Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

type Sing = SFirst :: First a -> Type
type Sing Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

type Sing = SLast :: Last a -> Type
type Sing Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

type Sing = SMax :: Max a -> Type
type Sing Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

type Sing = SMin :: Min a -> Type
type Sing Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

type Sing = SOption :: Option a -> Type
type Sing Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

type Sing = SWrappedMonoid :: WrappedMonoid m -> Type
type Sing Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

type Sing = SDual :: Dual a -> Type
type Sing Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

type Sing = SProduct :: Product a -> Type
type Sing Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

type Sing = SSum :: Sum a -> Type
type Sing Source # 
Instance details

Defined in Data.Singletons.Prelude.Monoid

type Sing = SFirst :: First a -> Type
type Sing Source # 
Instance details

Defined in Data.Singletons.Prelude.Monoid

type Sing = SLast :: Last a -> Type
type Sing Source # 
Instance details

Defined in Data.Singletons.Prelude.Instances

type Sing = SEither :: Either a b -> Type
type Sing Source # 
Instance details

Defined in Data.Singletons.Prelude.Instances

type Sing = STuple2 :: (a, b) -> Type
type Sing Source # 
Instance details

Defined in Data.Singletons.Internal

type Sing = SLambda :: (k1 ~> k2) -> Type
type Sing Source # 
Instance details

Defined in Data.Singletons.Internal

type Sing = SWrappedSing :: WrappedSing a -> Type
type Sing Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup

type Sing = SArg :: Arg a b -> Type
type Sing Source # 
Instance details

Defined in Data.Singletons.Sigma

type Sing = SSigma :: Sigma s t -> Type
type Sing Source # 
Instance details

Defined in Data.Singletons.Prelude.Instances

type Sing = STuple3 :: (a, b, c) -> Type
type Sing Source # 
Instance details

Defined in Data.Singletons.Prelude.Const

type Sing = SConst :: Const a b -> Type
type Sing Source # 
Instance details

Defined in Data.Singletons.Prelude.Instances

type Sing = STuple4 :: (a, b, c, d) -> Type
type Sing Source # 
Instance details

Defined in Data.Singletons.Prelude.Instances

type Sing = STuple5 :: (a, b, c, d, e) -> Type
type Sing Source # 
Instance details

Defined in Data.Singletons.Prelude.Instances

type Sing = STuple6 :: (a, b, c, d, e, f) -> Type
type Sing Source # 
Instance details

Defined in Data.Singletons.Prelude.Instances

type Sing = STuple7 :: (a, b, c, d, e, f, g) -> Type

data SNat (n :: Nat) Source #

Constructors

KnownNat n => SNat 

Instances

Instances details
Show (SNat n) 
Instance details

Defined in Data.Singletons.ShowSing

Methods

showsPrec :: Int -> SNat n -> ShowS

show :: SNat n -> String

showList :: [SNat n] -> ShowS

data SSymbol (n :: Symbol) Source #

Constructors

KnownSymbol n => SSym 

Instances

Instances details
Show (SSymbol s) 
Instance details

Defined in Data.Singletons.ShowSing

Methods

showsPrec :: Int -> SSymbol s -> ShowS

show :: SSymbol s -> String

showList :: [SSymbol s] -> ShowS

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

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

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

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

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

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

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

The singleton for error

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

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

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

The singleton for errorWithoutStackTrace.

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

The promotion of undefined.

sUndefined :: HasCallStack => a Source #

The singleton for undefined.

class KnownNat (n :: Nat) #

Minimal complete definition

natSing

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

class KnownSymbol (n :: Symbol) #

Minimal complete definition

symbolSing

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

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

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

The singleton analogue of (^) for Nats.

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

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

The singleton analogue of <=?

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

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

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

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

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

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

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

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

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

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

Equations

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

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

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

Equations

Quot a_6989586621679504147 a_6989586621679504149 = Apply (Apply DivSym0 a_6989586621679504147) a_6989586621679504149 

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

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

Equations

Rem a_6989586621679504137 a_6989586621679504139 = Apply (Apply ModSym0 a_6989586621679504137) a_6989586621679504139 

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

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

Equations

QuotRem a_6989586621679504157 a_6989586621679504159 = Apply (Apply DivModSym0 a_6989586621679504157) a_6989586621679504159 

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

Defunctionalization symbols

data ErrorSym0 :: forall k06989586621679481870 k6989586621679481871. (~>) k06989586621679481870 k6989586621679481871 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 k06989586621679481870 k6989586621679481871 -> Type) Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

Methods

suppressUnusedWarnings :: () Source #

type Apply (ErrorSym0 :: TyFun k0 k2 -> Type) (str6989586621679481872 :: k0) Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

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

type ErrorSym1 (str6989586621679481872 :: k06989586621679481870) = Error str6989586621679481872 Source #

data ErrorWithoutStackTraceSym0 :: forall k06989586621679482960 k6989586621679482961. (~>) k06989586621679482960 k6989586621679482961 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 k06989586621679482960 k6989586621679482961 -> Type) Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

Methods

suppressUnusedWarnings :: () Source #

type Apply (ErrorWithoutStackTraceSym0 :: TyFun k0 k2 -> Type) (str6989586621679482962 :: k0) Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

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

type ErrorWithoutStackTraceSym1 (str6989586621679482962 :: k06989586621679482960) = ErrorWithoutStackTrace str6989586621679482962 Source #

type UndefinedSym0 = Undefined Source #

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

Instances

Instances details
SuppressUnusedWarnings KnownNatSym0 Source # 
Instance details

Defined in Data.Singletons.TypeLits

Methods

suppressUnusedWarnings :: () Source #

type Apply KnownNatSym0 (n6989586621679482027 :: Nat) Source # 
Instance details

Defined in Data.Singletons.TypeLits

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

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

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

Instances

Instances details
SuppressUnusedWarnings KnownSymbolSym0 Source # 
Instance details

Defined in Data.Singletons.TypeLits

Methods

suppressUnusedWarnings :: () Source #

type Apply KnownSymbolSym0 (n6989586621679482093 :: Symbol) Source # 
Instance details

Defined in Data.Singletons.TypeLits

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

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

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

Instances

Instances details
SingI (^@#@$) Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

Methods

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

SuppressUnusedWarnings (^@#@$) Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

Methods

suppressUnusedWarnings :: () Source #

type Apply (^@#@$) (a3530822107858468865 :: Nat) Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

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

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

Instances

Instances details
SingI x => SingI ((^@#@$$) x :: TyFun Nat Nat -> Type) Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

Methods

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

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

Defined in Data.Singletons.TypeLits.Internal

Methods

suppressUnusedWarnings :: () Source #

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

Defined in Data.Singletons.TypeLits.Internal

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

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

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

Instances

Instances details
SingI (<=?@#@$) Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

Methods

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

SuppressUnusedWarnings (<=?@#@$) Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

Methods

suppressUnusedWarnings :: () Source #

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

Defined in Data.Singletons.TypeLits.Internal

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

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

Instances

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

Defined in Data.Singletons.TypeLits.Internal

Methods

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

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

Defined in Data.Singletons.TypeLits.Internal

Methods

suppressUnusedWarnings :: () Source #

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

Defined in Data.Singletons.TypeLits.Internal

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

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

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

Instances

Instances details
SingI Log2Sym0 Source # 
Instance details

Defined in Data.Singletons.TypeLits

Methods

sing :: Sing Log2Sym0 Source #

SuppressUnusedWarnings Log2Sym0 Source # 
Instance details

Defined in Data.Singletons.TypeLits

Methods

suppressUnusedWarnings :: () Source #

type Apply Log2Sym0 (a3530822107858468865 :: Nat) Source # 
Instance details

Defined in Data.Singletons.TypeLits

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

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

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

Instances

Instances details
SingI DivSym0 Source # 
Instance details

Defined in Data.Singletons.TypeLits

Methods

sing :: Sing DivSym0 Source #

SuppressUnusedWarnings DivSym0 Source # 
Instance details

Defined in Data.Singletons.TypeLits

Methods

suppressUnusedWarnings :: () Source #

type Apply DivSym0 (a3530822107858468865 :: Nat) Source # 
Instance details

Defined in Data.Singletons.TypeLits

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

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

Instances

Instances details
SingI x => SingI (DivSym1 x :: TyFun Nat Nat -> Type) Source # 
Instance details

Defined in Data.Singletons.TypeLits

Methods

sing :: Sing (DivSym1 x) Source #

SuppressUnusedWarnings (DivSym1 a3530822107858468865 :: TyFun Nat Nat -> Type) Source # 
Instance details

Defined in Data.Singletons.TypeLits

Methods

suppressUnusedWarnings :: () Source #

type Apply (DivSym1 a3530822107858468865 :: TyFun Nat Nat -> Type) (b3530822107858468866 :: Nat) Source # 
Instance details

Defined in Data.Singletons.TypeLits

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

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

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

Instances

Instances details
SingI ModSym0 Source # 
Instance details

Defined in Data.Singletons.TypeLits

Methods

sing :: Sing ModSym0 Source #

SuppressUnusedWarnings ModSym0 Source # 
Instance details

Defined in Data.Singletons.TypeLits

Methods

suppressUnusedWarnings :: () Source #

type Apply ModSym0 (a3530822107858468865 :: Nat) Source # 
Instance details

Defined in Data.Singletons.TypeLits

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

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

Instances

Instances details
SingI x => SingI (ModSym1 x :: TyFun Nat Nat -> Type) Source # 
Instance details

Defined in Data.Singletons.TypeLits

Methods

sing :: Sing (ModSym1 x) Source #

SuppressUnusedWarnings (ModSym1 a3530822107858468865 :: TyFun Nat Nat -> Type) Source # 
Instance details

Defined in Data.Singletons.TypeLits

Methods

suppressUnusedWarnings :: () Source #

type Apply (ModSym1 a3530822107858468865 :: TyFun Nat Nat -> Type) (b3530822107858468866 :: Nat) Source # 
Instance details

Defined in Data.Singletons.TypeLits

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

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

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

Instances

Instances details
SuppressUnusedWarnings DivModSym0 Source # 
Instance details

Defined in Data.Singletons.TypeLits

Methods

suppressUnusedWarnings :: () Source #

type Apply DivModSym0 (a6989586621679504167 :: Nat) Source # 
Instance details

Defined in Data.Singletons.TypeLits

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

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

Instances

Instances details
SuppressUnusedWarnings (DivModSym1 a6989586621679504167 :: TyFun Nat (Nat, Nat) -> Type) Source # 
Instance details

Defined in Data.Singletons.TypeLits

Methods

suppressUnusedWarnings :: () Source #

type Apply (DivModSym1 a6989586621679504167 :: TyFun Nat (Nat, Nat) -> Type) (a6989586621679504168 :: Nat) Source # 
Instance details

Defined in Data.Singletons.TypeLits

type Apply (DivModSym1 a6989586621679504167 :: TyFun Nat (Nat, Nat) -> Type) (a6989586621679504168 :: Nat) = DivMod a6989586621679504167 a6989586621679504168

type DivModSym2 (a6989586621679504167 :: Nat) (a6989586621679504168 :: Nat) = DivMod a6989586621679504167 a6989586621679504168 Source #

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

Instances

Instances details
SuppressUnusedWarnings QuotSym0 Source # 
Instance details

Defined in Data.Singletons.TypeLits

Methods

suppressUnusedWarnings :: () Source #

type Apply QuotSym0 (a6989586621679504151 :: Nat) Source # 
Instance details

Defined in Data.Singletons.TypeLits

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

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

Instances

Instances details
SuppressUnusedWarnings (QuotSym1 a6989586621679504151 :: TyFun Nat Nat -> Type) Source # 
Instance details

Defined in Data.Singletons.TypeLits

Methods

suppressUnusedWarnings :: () Source #

type Apply (QuotSym1 a6989586621679504151 :: TyFun Nat Nat -> Type) (a6989586621679504152 :: Nat) Source # 
Instance details

Defined in Data.Singletons.TypeLits

type Apply (QuotSym1 a6989586621679504151 :: TyFun Nat Nat -> Type) (a6989586621679504152 :: Nat) = Quot a6989586621679504151 a6989586621679504152

type QuotSym2 (a6989586621679504151 :: Nat) (a6989586621679504152 :: Nat) = Quot a6989586621679504151 a6989586621679504152 Source #

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

Instances

Instances details
SuppressUnusedWarnings RemSym0 Source # 
Instance details

Defined in Data.Singletons.TypeLits

Methods

suppressUnusedWarnings :: () Source #

type Apply RemSym0 (a6989586621679504141 :: Nat) Source # 
Instance details

Defined in Data.Singletons.TypeLits

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

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

Instances

Instances details
SuppressUnusedWarnings (RemSym1 a6989586621679504141 :: TyFun Nat Nat -> Type) Source # 
Instance details

Defined in Data.Singletons.TypeLits

Methods

suppressUnusedWarnings :: () Source #

type Apply (RemSym1 a6989586621679504141 :: TyFun Nat Nat -> Type) (a6989586621679504142 :: Nat) Source # 
Instance details

Defined in Data.Singletons.TypeLits

type Apply (RemSym1 a6989586621679504141 :: TyFun Nat Nat -> Type) (a6989586621679504142 :: Nat) = Rem a6989586621679504141 a6989586621679504142

type RemSym2 (a6989586621679504141 :: Nat) (a6989586621679504142 :: Nat) = Rem a6989586621679504141 a6989586621679504142 Source #

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

Instances

Instances details
SuppressUnusedWarnings QuotRemSym0 Source # 
Instance details

Defined in Data.Singletons.TypeLits

Methods

suppressUnusedWarnings :: () Source #

type Apply QuotRemSym0 (a6989586621679504161 :: Nat) Source # 
Instance details

Defined in Data.Singletons.TypeLits

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

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

Instances

Instances details
SuppressUnusedWarnings (QuotRemSym1 a6989586621679504161 :: TyFun Nat (Nat, Nat) -> Type) Source # 
Instance details

Defined in Data.Singletons.TypeLits

Methods

suppressUnusedWarnings :: () Source #

type Apply (QuotRemSym1 a6989586621679504161 :: TyFun Nat (Nat, Nat) -> Type) (a6989586621679504162 :: Nat) Source # 
Instance details

Defined in Data.Singletons.TypeLits

type Apply (QuotRemSym1 a6989586621679504161 :: TyFun Nat (Nat, Nat) -> Type) (a6989586621679504162 :: Nat) = QuotRem a6989586621679504161 a6989586621679504162

type QuotRemSym2 (a6989586621679504161 :: Nat) (a6989586621679504162 :: Nat) = QuotRem a6989586621679504161 a6989586621679504162 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