| Copyright | (C) 2014 Richard Eisenberg |
|---|---|
| License | BSD-style (see LICENSE) |
| Maintainer | Ryan Scott |
| Stability | experimental |
| Portability | non-portable |
| Safe Haskell | None |
| Language | Haskell2010 |
Data.Singletons.TypeLits
Description
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 k06989586621679484372 k6989586621679484371. (~>) k06989586621679484372 k6989586621679484371
- type ErrorSym1 (str6989586621679484373 :: k06989586621679484372) = Error str6989586621679484373
- data ErrorWithoutStackTraceSym0 :: forall k06989586621679485422 k6989586621679485421. (~>) k06989586621679485422 k6989586621679485421
- type ErrorWithoutStackTraceSym1 (str6989586621679485423 :: k06989586621679485422) = ErrorWithoutStackTrace str6989586621679485423
- type UndefinedSym0 = Undefined
- data KnownNatSym0 :: (~>) Nat Constraint
- type KnownNatSym1 (n6989586621679484627 :: Nat) = KnownNat n6989586621679484627
- data KnownSymbolSym0 :: (~>) Symbol Constraint
- type KnownSymbolSym1 (n6989586621679484567 :: Symbol) = KnownSymbol n6989586621679484567
- 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 (a6989586621679504739 :: Nat) :: (~>) Nat (Nat, Nat)
- type DivModSym2 (a6989586621679504739 :: Nat) (a6989586621679504740 :: Nat) = DivMod a6989586621679504739 a6989586621679504740
- data QuotSym0 :: (~>) Nat ((~>) Nat Nat)
- data QuotSym1 (a6989586621679504733 :: Nat) :: (~>) Nat Nat
- type QuotSym2 (a6989586621679504733 :: Nat) (a6989586621679504734 :: Nat) = Quot a6989586621679504733 a6989586621679504734
- data RemSym0 :: (~>) Nat ((~>) Nat Nat)
- data RemSym1 (a6989586621679504723 :: Nat) :: (~>) Nat Nat
- type RemSym2 (a6989586621679504723 :: Nat) (a6989586621679504724 :: Nat) = Rem a6989586621679504723 a6989586621679504724
- data QuotRemSym0 :: (~>) Nat ((~>) Nat (Nat, Nat))
- data QuotRemSym1 (a6989586621679504749 :: Nat) :: (~>) Nat (Nat, Nat)
- type QuotRemSym2 (a6989586621679504749 :: Nat) (a6989586621679504750 :: Nat) = QuotRem a6989586621679504749 a6989586621679504750
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 #
The singleton kind-indexed data family.
Instances
| SDecide k => TestCoercion (Sing :: k -> Type) # | |
Defined in Data.Singletons.Decide | |
| SDecide k => TestEquality (Sing :: k -> Type) # | |
Defined in Data.Singletons.Decide | |
| Show (SSymbol s) # | |
| Show (SNat n) # | |
| Eq (Sing a) # | |
| Ord (Sing a) # | |
| Show (Sing z) # | |
| (ShowSing a, ShowSing [a]) => Show (Sing z) # | |
| ShowSing a => Show (Sing z) # | |
| Show (Sing z) # | |
| (ShowSing a, ShowSing b) => Show (Sing z) # | |
| Show (Sing a) # | |
| Show (Sing z) # | |
| (ShowSing a, ShowSing b) => Show (Sing z) # | |
| (ShowSing a, ShowSing b, ShowSing c) => Show (Sing z) # | |
| (ShowSing a, ShowSing b, ShowSing c, ShowSing d) => Show (Sing z) # | |
| (ShowSing a, ShowSing b, ShowSing c, ShowSing d, ShowSing e) => Show (Sing z) # | |
| (ShowSing a, ShowSing b, ShowSing c, ShowSing d, ShowSing e, ShowSing f) => Show (Sing z) # | |
| (ShowSing a, ShowSing b, ShowSing c, ShowSing d, ShowSing e, ShowSing f, ShowSing g) => Show (Sing z) # | |
| Show (Sing z) # | |
| ShowSing a => Show (Sing z) # | |
| ShowSing a => Show (Sing z) # | |
| (ShowSing a, ShowSing b) => Show (Sing z) # | |
| ShowSing a => Show (Sing z) # | |
| ShowSing a => Show (Sing z) # | |
| ShowSing m => Show (Sing z) # | |
| ShowSing (Maybe a) => Show (Sing z) # | |
| ShowSing a => Show (Sing z) # | |
| ShowSing (Maybe a) => Show (Sing z) # | |
| ShowSing (Maybe a) => Show (Sing z) # | |
| ShowSing a => Show (Sing z) # | |
| ShowSing Bool => Show (Sing z) # | |
| ShowSing Bool => Show (Sing z) # | |
| ShowSing a => Show (Sing z) # | |
| ShowSing a => Show (Sing z) # | |
| (ShowSing a, ShowSing [a]) => Show (Sing z) # | |
| data Sing (a :: Bool) # | |
| data Sing (a :: Ordering) # | |
| data Sing (n :: Nat) # | |
| data Sing (n :: Symbol) # | |
Defined in Data.Singletons.TypeLits.Internal | |
| data Sing (a :: ()) # | |
Defined in Data.Singletons.Prelude.Instances | |
| data Sing (a :: Void) # | |
Defined in Data.Singletons.Prelude.Instances | |
| data Sing (a :: All) # | |
| data Sing (a :: Any) # | |
| data Sing (a :: PErrorMessage) # | |
Defined in Data.Singletons.TypeError data Sing (a :: PErrorMessage) where
| |
| data Sing (b :: [a]) # | |
| data Sing (b :: Maybe a) # | |
| newtype Sing (a :: TYPE rep) # | 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) # | |
| data Sing (b :: Max a) # | |
| data Sing (b :: First a) # | |
| data Sing (b :: Last a) # | |
| data Sing (a :: WrappedMonoid m) # | |
Defined in Data.Singletons.Prelude.Semigroup.Internal data Sing (a :: WrappedMonoid m) where
| |
| data Sing (b :: Option a) # | |
| data Sing (b :: Identity a) # | |
| data Sing (b :: First a) # | |
| data Sing (b :: Last a) # | |
| data Sing (b :: Dual a) # | |
| data Sing (b :: Sum a) # | |
| data Sing (b :: Product a) # | |
| data Sing (b :: Down a) # | |
| data Sing (b :: NonEmpty a) # | |
| data Sing (c :: Either a b) # | |
| data Sing (c :: (a, b)) # | |
| data Sing (c :: Arg a b) # | |
| newtype Sing (f :: k1 ~> k2) # | |
| data Sing (d :: (a, b, c)) # | |
| data Sing (c :: Const a b) # | |
| data Sing (e :: (a, b, c, d)) # | |
| data Sing (f :: (a, b, c, d, e)) # | |
| data Sing (g :: (a, b, c, d, e, f)) # | |
| data Sing (h :: (a, b, c, d, e, f, g)) # | |
Defined in Data.Singletons.Prelude.Instances | |
withKnownNat :: Sing n -> (KnownNat n => r) -> r #
Given a singleton for Nat, call something requiring a
KnownNat instance.
withKnownSymbol :: Sing n -> (KnownSymbol n => r) -> r #
Given a singleton for Symbol, call something requiring
a KnownSymbol instance.
type family Error (str :: k0) :: k where ... #
The promotion of error. This version is more poly-kinded for
easier use.
type family ErrorWithoutStackTrace (str :: k0) :: k where ... #
The promotion of errorWithoutStackTrace. This version is more
poly-kinded for easier use.
sErrorWithoutStackTrace :: Sing (str :: Symbol) -> a #
The singleton for errorWithoutStackTrace.
sUndefined :: HasCallStack => a #
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
Minimal complete definition
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
Minimal complete definition
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
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 #
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 ... #
Equations
| QuotRem a_6989586621679504745 a_6989586621679504747 = Apply (Apply DivModSym0 a_6989586621679504745) a_6989586621679504747 |
Defunctionalization symbols
data ErrorSym0 :: forall k06989586621679484372 k6989586621679484371. (~>) k06989586621679484372 k6989586621679484371 #
Instances
| SingI (ErrorSym0 :: TyFun Symbol a -> Type) # | |
Defined in Data.Singletons.TypeLits.Internal | |
| SuppressUnusedWarnings (ErrorSym0 :: TyFun k06989586621679484372 k6989586621679484371 -> Type) # | |
Defined in Data.Singletons.TypeLits.Internal Methods suppressUnusedWarnings :: () # | |
| type Apply (ErrorSym0 :: TyFun k0 k2 -> Type) (str6989586621679484373 :: k0) # | |
data ErrorWithoutStackTraceSym0 :: forall k06989586621679485422 k6989586621679485421. (~>) k06989586621679485422 k6989586621679485421 #
Instances
| SingI (ErrorWithoutStackTraceSym0 :: TyFun Symbol a -> Type) # | |
Defined in Data.Singletons.TypeLits.Internal Methods | |
| SuppressUnusedWarnings (ErrorWithoutStackTraceSym0 :: TyFun k06989586621679485422 k6989586621679485421 -> Type) # | |
Defined in Data.Singletons.TypeLits.Internal Methods suppressUnusedWarnings :: () # | |
| type Apply (ErrorWithoutStackTraceSym0 :: TyFun k0 k2 -> Type) (str6989586621679485423 :: k0) # | |
Defined in Data.Singletons.TypeLits.Internal type Apply (ErrorWithoutStackTraceSym0 :: TyFun k0 k2 -> Type) (str6989586621679485423 :: k0) = (ErrorWithoutStackTrace str6989586621679485423 :: k2) | |
type ErrorWithoutStackTraceSym1 (str6989586621679485423 :: k06989586621679485422) = ErrorWithoutStackTrace str6989586621679485423 #
type UndefinedSym0 = Undefined #
data KnownNatSym0 :: (~>) Nat Constraint #
Instances
| SuppressUnusedWarnings KnownNatSym0 # | |
Defined in Data.Singletons.TypeLits Methods suppressUnusedWarnings :: () # | |
| type Apply KnownNatSym0 (n6989586621679484627 :: Nat) # | |
Defined in Data.Singletons.TypeLits | |
type KnownNatSym1 (n6989586621679484627 :: Nat) = KnownNat n6989586621679484627 #
data KnownSymbolSym0 :: (~>) Symbol Constraint #
Instances
| SuppressUnusedWarnings KnownSymbolSym0 # | |
Defined in Data.Singletons.TypeLits Methods suppressUnusedWarnings :: () # | |
| type Apply KnownSymbolSym0 (n6989586621679484567 :: Symbol) # | |
Defined in Data.Singletons.TypeLits | |
type KnownSymbolSym1 (n6989586621679484567 :: Symbol) = KnownSymbol n6989586621679484567 #
data (^@#@$) :: (~>) Nat ((~>) Nat Nat) infixr 8 #
Instances
| SingI (^@#@$) # | |
Defined in Data.Singletons.TypeLits.Internal | |
| SuppressUnusedWarnings (^@#@$) # | |
Defined in Data.Singletons.TypeLits.Internal Methods suppressUnusedWarnings :: () # | |
| type Apply (^@#@$) (a3530822107858468865 :: Nat) # | |
Defined in Data.Singletons.TypeLits.Internal | |
data (^@#@$$) (a3530822107858468865 :: Nat) :: (~>) Nat Nat infixr 8 #
Instances
| SingI x => SingI ((^@#@$$) x :: TyFun Nat Nat -> Type) # | |
Defined in Data.Singletons.TypeLits.Internal | |
| SuppressUnusedWarnings ((^@#@$$) a3530822107858468865 :: TyFun Nat Nat -> Type) # | |
Defined in Data.Singletons.TypeLits.Internal Methods suppressUnusedWarnings :: () # | |
| type Apply ((^@#@$$) a3530822107858468865 :: TyFun Nat Nat -> Type) (b3530822107858468866 :: Nat) # | |
type (^@#@$$$) (a3530822107858468865 :: Nat) (b3530822107858468866 :: Nat) = (^) a3530822107858468865 b3530822107858468866 #
data (<=?@#@$) :: (~>) Nat ((~>) Nat Bool) infix 4 #
Instances
| SingI (<=?@#@$) # | |
Defined in Data.Singletons.TypeLits.Internal | |
| SuppressUnusedWarnings (<=?@#@$) # | |
Defined in Data.Singletons.TypeLits.Internal Methods suppressUnusedWarnings :: () # | |
| type Apply (<=?@#@$) (a3530822107858468865 :: Nat) # | |
Defined in Data.Singletons.TypeLits.Internal | |
data (<=?@#@$$) (a3530822107858468865 :: Nat) :: (~>) Nat Bool infix 4 #
Instances
| SingI x => SingI ((<=?@#@$$) x :: TyFun Nat Bool -> Type) # | |
Defined in Data.Singletons.TypeLits.Internal Methods sing :: Sing ((<=?@#@$$) x) # | |
| SuppressUnusedWarnings ((<=?@#@$$) a3530822107858468865 :: TyFun Nat Bool -> Type) # | |
Defined in Data.Singletons.TypeLits.Internal Methods suppressUnusedWarnings :: () # | |
| type Apply ((<=?@#@$$) a3530822107858468865 :: TyFun Nat Bool -> Type) (b3530822107858468866 :: Nat) # | |
Defined in Data.Singletons.TypeLits.Internal | |
type (<=?@#@$$$) (a3530822107858468865 :: Nat) (b3530822107858468866 :: Nat) = (<=?) a3530822107858468865 b3530822107858468866 #
data Log2Sym0 :: (~>) Nat Nat #
Instances
| SingI Log2Sym0 # | |
Defined in Data.Singletons.TypeLits | |
| SuppressUnusedWarnings Log2Sym0 # | |
Defined in Data.Singletons.TypeLits Methods suppressUnusedWarnings :: () # | |
| type Apply Log2Sym0 (a3530822107858468865 :: Nat) # | |
Defined in Data.Singletons.TypeLits | |
data DivSym0 :: (~>) Nat ((~>) Nat Nat) infixl 7 #
Instances
| SingI DivSym0 # | |
Defined in Data.Singletons.TypeLits | |
| SuppressUnusedWarnings DivSym0 # | |
Defined in Data.Singletons.TypeLits Methods suppressUnusedWarnings :: () # | |
| type Apply DivSym0 (a3530822107858468865 :: Nat) # | |
Defined in Data.Singletons.TypeLits | |
data DivSym1 (a3530822107858468865 :: Nat) :: (~>) Nat Nat infixl 7 #
Instances
| SingI x => SingI (DivSym1 x :: TyFun Nat Nat -> Type) # | |
Defined in Data.Singletons.TypeLits | |
| SuppressUnusedWarnings (DivSym1 a3530822107858468865 :: TyFun Nat Nat -> Type) # | |
Defined in Data.Singletons.TypeLits Methods suppressUnusedWarnings :: () # | |
| type Apply (DivSym1 a3530822107858468865 :: TyFun Nat Nat -> Type) (b3530822107858468866 :: Nat) # | |
type DivSym2 (a3530822107858468865 :: Nat) (b3530822107858468866 :: Nat) = Div a3530822107858468865 b3530822107858468866 #
data ModSym0 :: (~>) Nat ((~>) Nat Nat) infixl 7 #
Instances
| SingI ModSym0 # | |
Defined in Data.Singletons.TypeLits | |
| SuppressUnusedWarnings ModSym0 # | |
Defined in Data.Singletons.TypeLits Methods suppressUnusedWarnings :: () # | |
| type Apply ModSym0 (a3530822107858468865 :: Nat) # | |
Defined in Data.Singletons.TypeLits | |
data ModSym1 (a3530822107858468865 :: Nat) :: (~>) Nat Nat infixl 7 #
Instances
| SingI x => SingI (ModSym1 x :: TyFun Nat Nat -> Type) # | |
Defined in Data.Singletons.TypeLits | |
| SuppressUnusedWarnings (ModSym1 a3530822107858468865 :: TyFun Nat Nat -> Type) # | |
Defined in Data.Singletons.TypeLits Methods suppressUnusedWarnings :: () # | |
| type Apply (ModSym1 a3530822107858468865 :: TyFun Nat Nat -> Type) (b3530822107858468866 :: Nat) # | |
type ModSym2 (a3530822107858468865 :: Nat) (b3530822107858468866 :: Nat) = Mod a3530822107858468865 b3530822107858468866 #
data DivModSym0 :: (~>) Nat ((~>) Nat (Nat, Nat)) #
Instances
| SuppressUnusedWarnings DivModSym0 # | |
Defined in Data.Singletons.TypeLits Methods suppressUnusedWarnings :: () # | |
| type Apply DivModSym0 (a6989586621679504739 :: Nat) # | |
Defined in Data.Singletons.TypeLits | |
data DivModSym1 (a6989586621679504739 :: Nat) :: (~>) Nat (Nat, Nat) #
Instances
| SuppressUnusedWarnings (DivModSym1 a6989586621679504739 :: TyFun Nat (Nat, Nat) -> Type) # | |
Defined in Data.Singletons.TypeLits Methods suppressUnusedWarnings :: () # | |
| type Apply (DivModSym1 a6989586621679504739 :: TyFun Nat (Nat, Nat) -> Type) (a6989586621679504740 :: Nat) # | |
Defined in Data.Singletons.TypeLits | |
type DivModSym2 (a6989586621679504739 :: Nat) (a6989586621679504740 :: Nat) = DivMod a6989586621679504739 a6989586621679504740 #
data QuotSym0 :: (~>) Nat ((~>) Nat Nat) infixl 7 #
Instances
| SuppressUnusedWarnings QuotSym0 # | |
Defined in Data.Singletons.TypeLits Methods suppressUnusedWarnings :: () # | |
| type Apply QuotSym0 (a6989586621679504733 :: Nat) # | |
Defined in Data.Singletons.TypeLits | |
data QuotSym1 (a6989586621679504733 :: Nat) :: (~>) Nat Nat infixl 7 #
type QuotSym2 (a6989586621679504733 :: Nat) (a6989586621679504734 :: Nat) = Quot a6989586621679504733 a6989586621679504734 #
data RemSym0 :: (~>) Nat ((~>) Nat Nat) infixl 7 #
Instances
| SuppressUnusedWarnings RemSym0 # | |
Defined in Data.Singletons.TypeLits Methods suppressUnusedWarnings :: () # | |
| type Apply RemSym0 (a6989586621679504723 :: Nat) # | |
Defined in Data.Singletons.TypeLits | |
data RemSym1 (a6989586621679504723 :: Nat) :: (~>) Nat Nat infixl 7 #
type RemSym2 (a6989586621679504723 :: Nat) (a6989586621679504724 :: Nat) = Rem a6989586621679504723 a6989586621679504724 #
data QuotRemSym0 :: (~>) Nat ((~>) Nat (Nat, Nat)) #
Instances
| SuppressUnusedWarnings QuotRemSym0 # | |
Defined in Data.Singletons.TypeLits Methods suppressUnusedWarnings :: () # | |
| type Apply QuotRemSym0 (a6989586621679504749 :: Nat) # | |
Defined in Data.Singletons.TypeLits | |
data QuotRemSym1 (a6989586621679504749 :: Nat) :: (~>) Nat (Nat, Nat) #
Instances
| SuppressUnusedWarnings (QuotRemSym1 a6989586621679504749 :: TyFun Nat (Nat, Nat) -> Type) # | |
Defined in Data.Singletons.TypeLits Methods suppressUnusedWarnings :: () # | |
| type Apply (QuotRemSym1 a6989586621679504749 :: TyFun Nat (Nat, Nat) -> Type) (a6989586621679504750 :: Nat) # | |
Defined in Data.Singletons.TypeLits | |
type QuotRemSym2 (a6989586621679504749 :: Nat) (a6989586621679504750 :: Nat) = QuotRem a6989586621679504749 a6989586621679504750 #
Orphan instances
| Enum Nat # | |
| Eq Nat # | |
| 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. |
| Num Nat # | This bogus |
| Ord Nat # | |
| Ord Symbol # | |
| Show Nat # | |
| Show Symbol # | |
| IsString Symbol # | |
Methods fromString :: String -> Symbol # | |
| Semigroup Symbol # | |
| Monoid Symbol # | |