Copyright | (C) 2014 Richard Eisenberg |
---|---|
License | BSD-style (see LICENSE) |
Maintainer | Ryan Scott |
Stability | experimental |
Portability | non-portable |
Safe Haskell | None |
Language | Haskell2010 |
Defines and exports singletons useful for the Nat and Symbol kinds.
Synopsis
- data Nat
- data Symbol
- data family Sing :: k -> Type
- type SNat (x :: Nat) = Sing x
- type SSymbol (x :: Symbol) = Sing x
- withKnownNat :: Sing n -> (KnownNat n => r) -> r
- withKnownSymbol :: Sing n -> (KnownSymbol n => r) -> r
- type family Error (str :: k0) :: k where ...
- sError :: HasCallStack => Sing (str :: Symbol) -> a
- type family ErrorWithoutStackTrace (str :: k0) :: k where ...
- sErrorWithoutStackTrace :: Sing (str :: Symbol) -> a
- type family Undefined :: k where ...
- sUndefined :: HasCallStack => a
- class KnownNat (n :: Nat)
- natVal :: KnownNat n => proxy n -> Natural
- class KnownSymbol (n :: Symbol)
- symbolVal :: KnownSymbol n => proxy n -> String
- type family (a :: Nat) ^ (b :: Nat) :: Nat where ...
- (%^) :: Sing a -> Sing b -> Sing (a ^ b)
- type family (a :: Nat) <=? (b :: Nat) :: Bool where ...
- (%<=?) :: Sing a -> Sing b -> Sing (a <=? b)
- type family Log2 (a :: Nat) :: Nat where ...
- sLog2 :: Sing x -> Sing (Log2 x)
- type family Div (a :: Nat) (b :: Nat) :: Nat where ...
- sDiv :: Sing x -> Sing y -> Sing (Div x y)
- type family Mod (a :: Nat) (b :: Nat) :: Nat where ...
- sMod :: Sing x -> Sing y -> Sing (Mod x y)
- type family DivMod (a :: Nat) (a :: Nat) :: (Nat, Nat) where ...
- sDivMod :: Sing x -> Sing y -> Sing (DivMod x y)
- type family Quot (a :: Nat) (a :: Nat) :: Nat where ...
- sQuot :: Sing x -> Sing y -> Sing (Quot x y)
- type family Rem (a :: Nat) (a :: Nat) :: Nat where ...
- sRem :: Sing x -> Sing y -> Sing (Rem x y)
- type family QuotRem (a :: Nat) (a :: Nat) :: (Nat, Nat) where ...
- sQuotRem :: Sing x -> Sing y -> Sing (QuotRem x y)
- data ErrorSym0 :: forall k06989586621679468164 k6989586621679468163. (~>) k06989586621679468164 k6989586621679468163
- type ErrorSym1 (str6989586621679468165 :: k06989586621679468164) = Error str6989586621679468165
- data ErrorWithoutStackTraceSym0 :: forall k06989586621679469214 k6989586621679469213. (~>) k06989586621679469214 k6989586621679469213
- type ErrorWithoutStackTraceSym1 (str6989586621679469215 :: k06989586621679469214) = ErrorWithoutStackTrace str6989586621679469215
- type UndefinedSym0 = Undefined
- data KnownNatSym0 :: (~>) Nat Constraint
- type KnownNatSym1 (n6989586621679468419 :: Nat) = KnownNat n6989586621679468419
- data KnownSymbolSym0 :: (~>) Symbol Constraint
- type KnownSymbolSym1 (n6989586621679468359 :: Symbol) = KnownSymbol n6989586621679468359
- data (^@#@$) :: (~>) Nat ((~>) Nat Nat)
- data (^@#@$$) (a3530822107858468865 :: Nat) :: (~>) Nat Nat
- type (^@#@$$$) (a3530822107858468865 :: Nat) (b3530822107858468866 :: Nat) = (^) a3530822107858468865 b3530822107858468866
- data (<=?@#@$) :: (~>) Nat ((~>) Nat Bool)
- data (<=?@#@$$) (a3530822107858468865 :: Nat) :: (~>) Nat Bool
- type (<=?@#@$$$) (a3530822107858468865 :: Nat) (b3530822107858468866 :: Nat) = (<=?) a3530822107858468865 b3530822107858468866
- data Log2Sym0 :: (~>) Nat Nat
- type Log2Sym1 (a3530822107858468865 :: Nat) = Log2 a3530822107858468865
- data DivSym0 :: (~>) Nat ((~>) Nat Nat)
- data DivSym1 (a3530822107858468865 :: Nat) :: (~>) Nat Nat
- type DivSym2 (a3530822107858468865 :: Nat) (b3530822107858468866 :: Nat) = Div a3530822107858468865 b3530822107858468866
- data ModSym0 :: (~>) Nat ((~>) Nat Nat)
- data ModSym1 (a3530822107858468865 :: Nat) :: (~>) Nat Nat
- type ModSym2 (a3530822107858468865 :: Nat) (b3530822107858468866 :: Nat) = Mod a3530822107858468865 b3530822107858468866
- data DivModSym0 :: (~>) Nat ((~>) Nat (Nat, Nat))
- data DivModSym1 (a6989586621679487931 :: Nat) :: (~>) Nat (Nat, Nat)
- type DivModSym2 (a6989586621679487931 :: Nat) (a6989586621679487932 :: Nat) = DivMod a6989586621679487931 a6989586621679487932
- data QuotSym0 :: (~>) Nat ((~>) Nat Nat)
- data QuotSym1 (a6989586621679487925 :: Nat) :: (~>) Nat Nat
- type QuotSym2 (a6989586621679487925 :: Nat) (a6989586621679487926 :: Nat) = Quot a6989586621679487925 a6989586621679487926
- data RemSym0 :: (~>) Nat ((~>) Nat Nat)
- data RemSym1 (a6989586621679487915 :: Nat) :: (~>) Nat Nat
- type RemSym2 (a6989586621679487915 :: Nat) (a6989586621679487916 :: Nat) = Rem a6989586621679487915 a6989586621679487916
- data QuotRemSym0 :: (~>) Nat ((~>) Nat (Nat, Nat))
- data QuotRemSym1 (a6989586621679487941 :: Nat) :: (~>) Nat (Nat, Nat)
- type QuotRemSym2 (a6989586621679487941 :: Nat) (a6989586621679487942 :: Nat) = QuotRem a6989586621679487941 a6989586621679487942
Documentation
(Kind) This is the kind of type-level natural numbers.
Instances
(Kind) This is the kind of type-level symbols. Declared here because class IP needs it
Instances
data family Sing :: k -> Type Source #
The singleton kind-indexed data family.
Instances
SDecide k => TestCoercion (Sing :: k -> Type) Source # | |
Defined in Data.Singletons.Decide | |
SDecide k => TestEquality (Sing :: k -> Type) Source # | |
Defined in Data.Singletons.Decide | |
Show (SSymbol s) Source # | |
Show (SNat n) Source # | |
Eq (Sing a) Source # | |
Ord (Sing a) Source # | |
Show (Sing z) Source # | |
(ShowSing a, ShowSing [a]) => Show (Sing z) Source # | |
ShowSing a => Show (Sing z) Source # | |
Show (Sing z) Source # | |
(ShowSing a, ShowSing b) => Show (Sing z) Source # | |
Show (Sing a) Source # | |
Show (Sing z) Source # | |
(ShowSing a, ShowSing b) => Show (Sing z) Source # | |
(ShowSing a, ShowSing b, ShowSing c) => Show (Sing z) Source # | |
(ShowSing a, ShowSing b, ShowSing c, ShowSing d) => Show (Sing z) Source # | |
(ShowSing a, ShowSing b, ShowSing c, ShowSing d, ShowSing e) => Show (Sing z) Source # | |
(ShowSing a, ShowSing b, ShowSing c, ShowSing d, ShowSing e, ShowSing f) => Show (Sing z) Source # | |
(ShowSing a, ShowSing b, ShowSing c, ShowSing d, ShowSing e, ShowSing f, ShowSing g) => Show (Sing z) Source # | |
Show (Sing z) Source # | |
ShowSing a => Show (Sing z) Source # | |
ShowSing a => Show (Sing z) Source # | |
(ShowSing a, ShowSing b) => Show (Sing z) Source # | |
ShowSing a => Show (Sing z) Source # | |
ShowSing a => Show (Sing z) Source # | |
ShowSing m => Show (Sing z) Source # | |
ShowSing (Maybe a) => Show (Sing z) Source # | |
ShowSing a => Show (Sing z) Source # | |
ShowSing (Maybe a) => Show (Sing z) Source # | |
ShowSing (Maybe a) => Show (Sing z) Source # | |
ShowSing a => Show (Sing z) Source # | |
ShowSing Bool => Show (Sing z) Source # | |
ShowSing Bool => Show (Sing z) Source # | |
ShowSing a => Show (Sing z) Source # | |
ShowSing a => Show (Sing z) Source # | |
(ShowSing a, ShowSing [a]) => Show (Sing z) Source # | |
data Sing (a :: Bool) Source # | |
data Sing (a :: Ordering) Source # | |
data Sing (n :: Nat) Source # | |
data Sing (n :: Symbol) Source # | |
Defined in Data.Singletons.TypeLits.Internal | |
data Sing (a :: ()) Source # | |
Defined in Data.Singletons.Prelude.Instances | |
data Sing (a :: Void) Source # | |
Defined in Data.Singletons.Prelude.Instances | |
data Sing (a :: All) Source # | |
data Sing (a :: Any) Source # | |
data Sing (a :: PErrorMessage) Source # | |
Defined in Data.Singletons.TypeError data Sing (a :: PErrorMessage) where
| |
data Sing (b :: [a]) Source # | |
data Sing (b :: Maybe a) Source # | |
data Sing (a :: TYPE rep) Source # | A choice of singleton for the kind Conceivably, one could generalize this instance to `Sing :: k -> Type` for
any kind We cannot produce explicit singleton values for everything in |
Defined in Data.Singletons.TypeRepTYPE | |
data Sing (b :: Min a) Source # | |
data Sing (b :: Max a) Source # | |
data Sing (b :: First a) Source # | |
data Sing (b :: Last a) Source # | |
data Sing (a :: WrappedMonoid m) Source # | |
Defined in Data.Singletons.Prelude.Semigroup.Internal data Sing (a :: WrappedMonoid m) where
| |
data Sing (b :: Option a) Source # | |
data Sing (b :: Identity a) Source # | |
data Sing (b :: First a) Source # | |
data Sing (b :: Last a) Source # | |
data Sing (b :: Dual a) Source # | |
data Sing (b :: Sum a) Source # | |
data Sing (b :: Product a) Source # | |
data Sing (b :: Down a) Source # | |
data Sing (b :: NonEmpty a) Source # | |
data Sing (c :: Either a b) Source # | |
data Sing (c :: (a, b)) Source # | |
data Sing (c :: Arg a b) Source # | |
data Sing (f :: k1 ~> k2) Source # | |
data Sing (d :: (a, b, c)) Source # | |
data Sing (c :: Const a b) Source # | |
data Sing (e :: (a, b, c, d)) Source # | |
data Sing (f :: (a, b, c, d, e)) Source # | |
data Sing (g :: (a, b, c, d, e, f)) Source # | |
data Sing (h :: (a, b, c, d, e, f, g)) Source # | |
Defined in Data.Singletons.Prelude.Instances |
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.
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
.
sUndefined :: HasCallStack => a Source #
The singleton for undefined
.
This class gives the integer associated with a type-level natural. There are instances of the class for every concrete literal: 0, 1, 2, etc.
Since: base-4.7.0.0
natSing
class KnownSymbol (n :: Symbol) #
This class gives the string associated with a type-level symbol. There are instances of the class for every concrete literal: "hello", etc.
Since: base-4.7.0.0
symbolSing
symbolVal :: KnownSymbol n => proxy n -> String #
Since: base-4.7.0.0
type family (a :: Nat) ^ (b :: Nat) :: Nat where ... infixr 8 #
Exponentiation of type-level naturals.
Since: base-4.7.0.0
(%^) :: Sing a -> Sing b -> Sing (a ^ b) infixr 8 Source #
The singleton analogue of '(TN.^)' for Nat
s.
type family (a :: Nat) <=? (b :: Nat) :: Bool where ... infix 4 #
Comparison of type-level naturals, as a function.
NOTE: The functionality for this function should be subsumed
by CmpNat
, so this might go away in the future.
Please let us know, if you encounter discrepancies between the two.
(%<=?) :: Sing a -> Sing b -> Sing (a <=? b) infix 4 Source #
The singleton analogue of <=?
Note that, because of historical reasons in GHC's Nat
API, <=?
is incompatible (unification-wise) with <=
and the PEq
, SEq
,
POrd
, and SOrd
instances for Nat
. (a
does not
imply anything about <=?
b) ~ 'Truea
or any other <=
bPEq
/ POrd
relationships.
(Be aware that <=
in the paragraph above refers to <=
from the
POrd
typeclass, exported from Data.Singletons.Prelude.Ord, and not
the <=
from GHC.TypeNats. The latter is simply a type alias for
(a
.)<=?
b) ~ 'True
This is provided here for the sake of completeness and for compatibility
with libraries with APIs built around <=?
. New code should use
CmpNat
, exposed through this library through the POrd
and SOrd
instances for Nat
.
type family Log2 (a :: Nat) :: Nat where ... #
Log base 2 (round down) of natural numbers.
Log 0
is undefined (i.e., it cannot be reduced).
Since: base-4.11.0.0
type family Div (a :: Nat) (b :: Nat) :: Nat where ... infixl 7 #
Division (round down) of natural numbers.
Div x 0
is undefined (i.e., it cannot be reduced).
Since: base-4.11.0.0
type family Mod (a :: Nat) (b :: Nat) :: Nat where ... infixl 7 #
Modulus of natural numbers.
Mod x 0
is undefined (i.e., it cannot be reduced).
Since: base-4.11.0.0
type family QuotRem (a :: Nat) (a :: Nat) :: (Nat, Nat) where ... Source #
QuotRem a_6989586621679487937 a_6989586621679487939 = Apply (Apply DivModSym0 a_6989586621679487937) a_6989586621679487939 |
Defunctionalization symbols
data ErrorSym0 :: forall k06989586621679468164 k6989586621679468163. (~>) k06989586621679468164 k6989586621679468163 Source #
Instances
SingI (ErrorSym0 :: TyFun Symbol a -> Type) Source # | |
SuppressUnusedWarnings (ErrorSym0 :: TyFun k06989586621679468164 k6989586621679468163 -> Type) Source # | |
Defined in Data.Singletons.TypeLits.Internal suppressUnusedWarnings :: () Source # | |
type Apply (ErrorSym0 :: TyFun k0 k2 -> Type) (str6989586621679468165 :: k0) Source # | |
type ErrorSym1 (str6989586621679468165 :: k06989586621679468164) = Error str6989586621679468165 Source #
data ErrorWithoutStackTraceSym0 :: forall k06989586621679469214 k6989586621679469213. (~>) k06989586621679469214 k6989586621679469213 Source #
Instances
SingI (ErrorWithoutStackTraceSym0 :: TyFun Symbol a -> Type) Source # | |
Defined in Data.Singletons.TypeLits.Internal | |
SuppressUnusedWarnings (ErrorWithoutStackTraceSym0 :: TyFun k06989586621679469214 k6989586621679469213 -> Type) Source # | |
Defined in Data.Singletons.TypeLits.Internal suppressUnusedWarnings :: () Source # | |
type Apply (ErrorWithoutStackTraceSym0 :: TyFun k0 k2 -> Type) (str6989586621679469215 :: k0) Source # | |
Defined in Data.Singletons.TypeLits.Internal type Apply (ErrorWithoutStackTraceSym0 :: TyFun k0 k2 -> Type) (str6989586621679469215 :: k0) = (ErrorWithoutStackTrace str6989586621679469215 :: k2) |
type ErrorWithoutStackTraceSym1 (str6989586621679469215 :: k06989586621679469214) = ErrorWithoutStackTrace str6989586621679469215 Source #
type UndefinedSym0 = Undefined Source #
data KnownNatSym0 :: (~>) Nat Constraint Source #
Instances
SuppressUnusedWarnings KnownNatSym0 Source # | |
Defined in Data.Singletons.TypeLits suppressUnusedWarnings :: () Source # | |
type Apply KnownNatSym0 (n6989586621679468419 :: Nat) Source # | |
Defined in Data.Singletons.TypeLits |
type KnownNatSym1 (n6989586621679468419 :: Nat) = KnownNat n6989586621679468419 Source #
data KnownSymbolSym0 :: (~>) Symbol Constraint Source #
Instances
SuppressUnusedWarnings KnownSymbolSym0 Source # | |
Defined in Data.Singletons.TypeLits suppressUnusedWarnings :: () Source # | |
type Apply KnownSymbolSym0 (n6989586621679468359 :: Symbol) Source # | |
Defined in Data.Singletons.TypeLits |
type KnownSymbolSym1 (n6989586621679468359 :: Symbol) = KnownSymbol n6989586621679468359 Source #
data (^@#@$) :: (~>) Nat ((~>) Nat Nat) infixr 8 Source #
Instances
SingI (^@#@$) Source # | |
SuppressUnusedWarnings (^@#@$) Source # | |
Defined in Data.Singletons.TypeLits.Internal suppressUnusedWarnings :: () Source # | |
type Apply (^@#@$) (a3530822107858468865 :: Nat) Source # | |
Defined in Data.Singletons.TypeLits.Internal |
data (^@#@$$) (a3530822107858468865 :: Nat) :: (~>) Nat Nat infixr 8 Source #
Instances
SingI x => SingI ((^@#@$$) x :: TyFun Nat Nat -> Type) Source # | |
SuppressUnusedWarnings ((^@#@$$) a3530822107858468865 :: TyFun Nat Nat -> Type) Source # | |
Defined in Data.Singletons.TypeLits.Internal suppressUnusedWarnings :: () Source # | |
type Apply ((^@#@$$) a3530822107858468865 :: TyFun Nat Nat -> Type) (b3530822107858468866 :: Nat) Source # | |
type (^@#@$$$) (a3530822107858468865 :: Nat) (b3530822107858468866 :: Nat) = (^) a3530822107858468865 b3530822107858468866 Source #
data (<=?@#@$) :: (~>) Nat ((~>) Nat Bool) infix 4 Source #
Instances
SingI (<=?@#@$) Source # | |
SuppressUnusedWarnings (<=?@#@$) Source # | |
Defined in Data.Singletons.TypeLits.Internal suppressUnusedWarnings :: () Source # | |
type Apply (<=?@#@$) (a3530822107858468865 :: Nat) Source # | |
Defined in Data.Singletons.TypeLits.Internal |
data (<=?@#@$$) (a3530822107858468865 :: Nat) :: (~>) Nat Bool infix 4 Source #
Instances
SingI x => SingI ((<=?@#@$$) x :: TyFun Nat Bool -> Type) Source # | |
Defined in Data.Singletons.TypeLits.Internal sing :: Sing ((<=?@#@$$) x) Source # | |
SuppressUnusedWarnings ((<=?@#@$$) a3530822107858468865 :: TyFun Nat Bool -> Type) Source # | |
Defined in Data.Singletons.TypeLits.Internal suppressUnusedWarnings :: () Source # | |
type Apply ((<=?@#@$$) a3530822107858468865 :: TyFun Nat Bool -> Type) (b3530822107858468866 :: Nat) Source # | |
Defined in Data.Singletons.TypeLits.Internal |
type (<=?@#@$$$) (a3530822107858468865 :: Nat) (b3530822107858468866 :: Nat) = (<=?) a3530822107858468865 b3530822107858468866 Source #
data Log2Sym0 :: (~>) Nat Nat Source #
Instances
SingI Log2Sym0 Source # | |
SuppressUnusedWarnings Log2Sym0 Source # | |
Defined in Data.Singletons.TypeLits suppressUnusedWarnings :: () Source # | |
type Apply Log2Sym0 (a3530822107858468865 :: Nat) Source # | |
Defined in Data.Singletons.TypeLits |
data DivSym0 :: (~>) Nat ((~>) Nat Nat) infixl 7 Source #
Instances
SingI DivSym0 Source # | |
SuppressUnusedWarnings DivSym0 Source # | |
Defined in Data.Singletons.TypeLits suppressUnusedWarnings :: () Source # | |
type Apply DivSym0 (a3530822107858468865 :: Nat) Source # | |
Defined in Data.Singletons.TypeLits |
data DivSym1 (a3530822107858468865 :: Nat) :: (~>) Nat Nat infixl 7 Source #
Instances
SingI x => SingI (DivSym1 x :: TyFun Nat Nat -> Type) Source # | |
SuppressUnusedWarnings (DivSym1 a3530822107858468865 :: TyFun Nat Nat -> Type) Source # | |
Defined in Data.Singletons.TypeLits suppressUnusedWarnings :: () Source # | |
type Apply (DivSym1 a3530822107858468865 :: TyFun Nat Nat -> Type) (b3530822107858468866 :: Nat) Source # | |
type DivSym2 (a3530822107858468865 :: Nat) (b3530822107858468866 :: Nat) = Div a3530822107858468865 b3530822107858468866 Source #
data ModSym0 :: (~>) Nat ((~>) Nat Nat) infixl 7 Source #
Instances
SingI ModSym0 Source # | |
SuppressUnusedWarnings ModSym0 Source # | |
Defined in Data.Singletons.TypeLits suppressUnusedWarnings :: () Source # | |
type Apply ModSym0 (a3530822107858468865 :: Nat) Source # | |
Defined in Data.Singletons.TypeLits |
data ModSym1 (a3530822107858468865 :: Nat) :: (~>) Nat Nat infixl 7 Source #
Instances
SingI x => SingI (ModSym1 x :: TyFun Nat Nat -> Type) Source # | |
SuppressUnusedWarnings (ModSym1 a3530822107858468865 :: TyFun Nat Nat -> Type) Source # | |
Defined in Data.Singletons.TypeLits suppressUnusedWarnings :: () Source # | |
type Apply (ModSym1 a3530822107858468865 :: TyFun Nat Nat -> Type) (b3530822107858468866 :: Nat) Source # | |
type ModSym2 (a3530822107858468865 :: Nat) (b3530822107858468866 :: Nat) = Mod a3530822107858468865 b3530822107858468866 Source #
data DivModSym0 :: (~>) Nat ((~>) Nat (Nat, Nat)) Source #
Instances
SuppressUnusedWarnings DivModSym0 Source # | |
Defined in Data.Singletons.TypeLits suppressUnusedWarnings :: () Source # | |
type Apply DivModSym0 (a6989586621679487931 :: Nat) Source # | |
Defined in Data.Singletons.TypeLits |
data DivModSym1 (a6989586621679487931 :: Nat) :: (~>) Nat (Nat, Nat) Source #
Instances
SuppressUnusedWarnings (DivModSym1 a6989586621679487931 :: TyFun Nat (Nat, Nat) -> Type) Source # | |
Defined in Data.Singletons.TypeLits suppressUnusedWarnings :: () Source # | |
type Apply (DivModSym1 a6989586621679487931 :: TyFun Nat (Nat, Nat) -> Type) (a6989586621679487932 :: Nat) Source # | |
Defined in Data.Singletons.TypeLits |
type DivModSym2 (a6989586621679487931 :: Nat) (a6989586621679487932 :: Nat) = DivMod a6989586621679487931 a6989586621679487932 Source #
data QuotSym0 :: (~>) Nat ((~>) Nat Nat) infixl 7 Source #
Instances
SuppressUnusedWarnings QuotSym0 Source # | |
Defined in Data.Singletons.TypeLits suppressUnusedWarnings :: () Source # | |
type Apply QuotSym0 (a6989586621679487925 :: Nat) Source # | |
Defined in Data.Singletons.TypeLits |
data QuotSym1 (a6989586621679487925 :: Nat) :: (~>) Nat Nat infixl 7 Source #
type QuotSym2 (a6989586621679487925 :: Nat) (a6989586621679487926 :: Nat) = Quot a6989586621679487925 a6989586621679487926 Source #
data RemSym0 :: (~>) Nat ((~>) Nat Nat) infixl 7 Source #
Instances
SuppressUnusedWarnings RemSym0 Source # | |
Defined in Data.Singletons.TypeLits suppressUnusedWarnings :: () Source # | |
type Apply RemSym0 (a6989586621679487915 :: Nat) Source # | |
Defined in Data.Singletons.TypeLits |
data RemSym1 (a6989586621679487915 :: Nat) :: (~>) Nat Nat infixl 7 Source #
type RemSym2 (a6989586621679487915 :: Nat) (a6989586621679487916 :: Nat) = Rem a6989586621679487915 a6989586621679487916 Source #
data QuotRemSym0 :: (~>) Nat ((~>) Nat (Nat, Nat)) Source #
Instances
SuppressUnusedWarnings QuotRemSym0 Source # | |
Defined in Data.Singletons.TypeLits suppressUnusedWarnings :: () Source # | |
type Apply QuotRemSym0 (a6989586621679487941 :: Nat) Source # | |
Defined in Data.Singletons.TypeLits |
data QuotRemSym1 (a6989586621679487941 :: Nat) :: (~>) Nat (Nat, Nat) Source #
Instances
SuppressUnusedWarnings (QuotRemSym1 a6989586621679487941 :: TyFun Nat (Nat, Nat) -> Type) Source # | |
Defined in Data.Singletons.TypeLits suppressUnusedWarnings :: () Source # | |
type Apply (QuotRemSym1 a6989586621679487941 :: TyFun Nat (Nat, Nat) -> Type) (a6989586621679487942 :: Nat) Source # | |
Defined in Data.Singletons.TypeLits |
type QuotRemSym2 (a6989586621679487941 :: Nat) (a6989586621679487942 :: Nat) = QuotRem a6989586621679487941 a6989586621679487942 Source #
Orphan instances
Enum Nat Source # | |
Eq Nat Source # | |
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. |
Num Nat Source # | This bogus |
Ord Nat Source # | |
Ord Symbol Source # | |
Show Nat Source # | |
Show Symbol Source # | |
IsString Symbol Source # | |
fromString :: String -> Symbol # | |
Semigroup Symbol Source # | |
Monoid Symbol Source # | |