| Copyright | (C) 2014 Richard Eisenberg |
|---|---|
| License | BSD-style (see LICENSE) |
| Maintainer | Ryan Scott |
| Stability | experimental |
| Portability | non-portable |
| Safe Haskell | Safe-Inferred |
| Language | Haskell2010 |
GHC.TypeLits.Singletons
Description
Defines and exports singletons useful for the Natural, Symbol, and Char kinds.
Synopsis
- data Natural
- data Symbol
- data Char
- type family Sing :: k -> Type
- data SNat (n :: Natural) = KnownNat n => SNat
- data SSymbol (n :: Symbol) = KnownSymbol n => SSym
- data SChar (c :: Char) = KnownChar c => SChar
- withKnownNat :: Sing n -> (KnownNat n => r) -> r
- withKnownSymbol :: Sing n -> (KnownSymbol n => r) -> r
- withKnownChar :: Sing n -> (KnownChar n => r) -> r
- type family Error (str :: k0) :: k where ...
- sError :: HasCallStack => Sing (str :: Symbol) -> a
- type family ErrorWithoutStackTrace (str :: k0) :: k where ...
- sErrorWithoutStackTrace :: Sing (str :: Symbol) -> a
- type family Undefined :: k where ...
- sUndefined :: HasCallStack => a
- class KnownNat (n :: Nat)
- natVal :: forall (n :: Nat) proxy. KnownNat n => proxy n -> Natural
- class KnownSymbol (n :: Symbol)
- symbolVal :: forall (n :: Symbol) proxy. KnownSymbol n => proxy n -> String
- class KnownChar (n :: Char)
- charVal :: forall (n :: Char) proxy. KnownChar n => proxy n -> Char
- type family (a :: Natural) ^ (b :: Natural) :: Natural where ...
- (%^) :: Sing a -> Sing b -> Sing (a ^ b)
- type (<=?) (m :: k) (n :: k) = OrdCond (Compare m n) 'True 'True 'False
- (%<=?) :: forall (a :: Natural) (b :: Natural). Sing a -> Sing b -> Sing (a <=? b)
- type family Log2 (a :: Natural) :: Natural where ...
- sLog2 :: Sing x -> Sing (Log2 x)
- type family Div (a :: Natural) (b :: Natural) :: Natural where ...
- sDiv :: Sing x -> Sing y -> Sing (Div x y)
- type family Mod (a :: Natural) (b :: Natural) :: Natural where ...
- sMod :: Sing x -> Sing y -> Sing (Mod x y)
- type family DivMod (a :: Natural) (a :: Natural) :: (Natural, Natural) where ...
- sDivMod :: Sing x -> Sing y -> Sing (DivMod x y)
- type family Quot (a :: Natural) (a :: Natural) :: Natural where ...
- sQuot :: Sing x -> Sing y -> Sing (Quot x y)
- type family Rem (a :: Natural) (a :: Natural) :: Natural where ...
- sRem :: Sing x -> Sing y -> Sing (Rem x y)
- type family QuotRem (a :: Natural) (a :: Natural) :: (Natural, Natural) where ...
- sQuotRem :: Sing x -> Sing y -> Sing (QuotRem x y)
- consSymbol :: Char -> String -> String
- type family ConsSymbol (a :: Char) (b :: Symbol) :: Symbol where ...
- sConsSymbol :: Sing x -> Sing y -> Sing (ConsSymbol x y)
- unconsSymbol :: String -> Maybe (Char, String)
- type family UnconsSymbol (a :: Symbol) :: Maybe (Char, Symbol) where ...
- sUnconsSymbol :: Sing x -> Sing (UnconsSymbol x)
- charToNat :: Char -> Natural
- type family CharToNat (a :: Char) :: Natural where ...
- sCharToNat :: Sing x -> Sing (CharToNat x)
- natToChar :: Natural -> Char
- type family NatToChar (a :: Natural) :: Char where ...
- sNatToChar :: Sing x -> Sing (NatToChar x)
- data ErrorSym0 :: (~>) k0 k
- type family ErrorSym1 (a6989586621679545715 :: k0) :: k where ...
- data ErrorWithoutStackTraceSym0 :: (~>) k0 k
- type family ErrorWithoutStackTraceSym1 (a6989586621679545983 :: k0) :: k where ...
- type family UndefinedSym0 :: k where ...
- data KnownNatSym0 :: (~>) Nat Constraint
- type family KnownNatSym1 (a6989586621679557763 :: Nat) :: Constraint where ...
- data KnownSymbolSym0 :: (~>) Symbol Constraint
- type family KnownSymbolSym1 (a6989586621679557765 :: Symbol) :: Constraint where ...
- data KnownCharSym0 :: (~>) Char Constraint
- type family KnownCharSym1 (a6989586621679557767 :: Char) :: Constraint where ...
- data (^@#@$) :: (~>) Natural ((~>) Natural Natural)
- data (^@#@$$) (a6989586621679546930 :: Natural) :: (~>) Natural Natural
- type family (a6989586621679546930 :: Natural) ^@#@$$$ (a6989586621679546931 :: Natural) :: Natural where ...
- data (<=?@#@$) :: (~>) k ((~>) k Bool)
- data (<=?@#@$$) (a6989586621679547349 :: k) :: (~>) k Bool
- type family (a6989586621679547349 :: k) <=?@#@$$$ (a6989586621679547350 :: k) :: Bool where ...
- data Log2Sym0 :: (~>) Natural Natural
- type family Log2Sym1 (a6989586621679558354 :: Natural) :: Natural where ...
- data DivSym0 :: (~>) Natural ((~>) Natural Natural)
- data DivSym1 (a6989586621679558584 :: Natural) :: (~>) Natural Natural
- type family DivSym2 (a6989586621679558584 :: Natural) (a6989586621679558585 :: Natural) :: Natural where ...
- data ModSym0 :: (~>) Natural ((~>) Natural Natural)
- data ModSym1 (a6989586621679559017 :: Natural) :: (~>) Natural Natural
- type family ModSym2 (a6989586621679559017 :: Natural) (a6989586621679559018 :: Natural) :: Natural where ...
- data DivModSym0 :: (~>) Natural ((~>) Natural (Natural, Natural))
- data DivModSym1 (a6989586621679559612 :: Natural) :: (~>) Natural (Natural, Natural)
- type family DivModSym2 (a6989586621679559612 :: Natural) (a6989586621679559613 :: Natural) :: (Natural, Natural) where ...
- data QuotSym0 :: (~>) Natural ((~>) Natural Natural)
- data QuotSym1 (a6989586621679559594 :: Natural) :: (~>) Natural Natural
- type family QuotSym2 (a6989586621679559594 :: Natural) (a6989586621679559595 :: Natural) :: Natural where ...
- data RemSym0 :: (~>) Natural ((~>) Natural Natural)
- data RemSym1 (a6989586621679559583 :: Natural) :: (~>) Natural Natural
- type family RemSym2 (a6989586621679559583 :: Natural) (a6989586621679559584 :: Natural) :: Natural where ...
- data QuotRemSym0 :: (~>) Natural ((~>) Natural (Natural, Natural))
- data QuotRemSym1 (a6989586621679559605 :: Natural) :: (~>) Natural (Natural, Natural)
- type family QuotRemSym2 (a6989586621679559605 :: Natural) (a6989586621679559606 :: Natural) :: (Natural, Natural) where ...
- data ConsSymbolSym0 :: (~>) Char ((~>) Symbol Symbol)
- data ConsSymbolSym1 (a6989586621679560776 :: Char) :: (~>) Symbol Symbol
- type family ConsSymbolSym2 (a6989586621679560776 :: Char) (a6989586621679560777 :: Symbol) :: Symbol where ...
- data UnconsSymbolSym0 :: (~>) Symbol (Maybe (Char, Symbol))
- type family UnconsSymbolSym1 (a6989586621679561235 :: Symbol) :: Maybe (Char, Symbol) where ...
- data CharToNatSym0 :: (~>) Char Natural
- type family CharToNatSym1 (a6989586621679561453 :: Char) :: Natural where ...
- data NatToCharSym0 :: (~>) Natural Char
- type family NatToCharSym1 (a6989586621679561676 :: Natural) :: Char where ...
Documentation
Natural number
Invariant: numbers <= 0xffffffffffffffff use the NS constructor
Instances
| Enum Natural | Since: base-4.8.0.0 |
| Ix Natural | Since: base-4.8.0.0 |
Defined in GHC.Ix | |
| Num Natural | Note that Since: base-4.8.0.0 |
| Read Natural | Since: base-4.8.0.0 |
| Integral Natural | Since: base-4.8.0.0 |
Defined in GHC.Real | |
| Real Natural | Since: base-4.8.0.0 |
Defined in GHC.Real Methods toRational :: Natural -> Rational # | |
| Show Natural | Since: base-4.8.0.0 |
| Eq Natural | |
| Ord Natural | |
| SingKind Natural | |
| SDecide Natural Source # | |
| PEq Natural Source # | |
| SEq Natural Source # | |
| POrd Natural Source # | |
| SOrd Natural Source # | |
Defined in GHC.TypeLits.Singletons.Internal Methods sCompare :: forall (t :: Natural) (t :: Natural). Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source # (%<) :: forall (t :: Natural) (t :: Natural). Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source # (%<=) :: forall (t :: Natural) (t :: Natural). Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source # (%>) :: forall (t :: Natural) (t :: Natural). Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source # (%>=) :: forall (t :: Natural) (t :: Natural). Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source # sMax :: forall (t :: Natural) (t :: Natural). Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source # sMin :: forall (t :: Natural) (t :: Natural). Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source # | |
| PEnum Natural Source # | |
| SEnum Natural Source # | |
Defined in Data.Singletons.Base.Enum Methods sSucc :: forall (t :: Natural). Sing t -> Sing (Apply SuccSym0 t) Source # sPred :: forall (t :: Natural). Sing t -> Sing (Apply PredSym0 t) Source # sToEnum :: forall (t :: Natural). Sing t -> Sing (Apply ToEnumSym0 t) Source # sFromEnum :: forall (t :: Natural). Sing t -> Sing (Apply FromEnumSym0 t) Source # sEnumFromTo :: forall (t :: Natural) (t :: Natural). Sing t -> Sing t -> Sing (Apply (Apply EnumFromToSym0 t) t) Source # sEnumFromThenTo :: forall (t :: Natural) (t :: Natural) (t :: Natural). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply EnumFromThenToSym0 t) t) t) Source # | |
| PNum Natural Source # | |
| SNum Natural Source # | |
Defined in GHC.Num.Singletons Methods (%+) :: forall (t :: Natural) (t :: Natural). Sing t -> Sing t -> Sing (Apply (Apply (+@#@$) t) t) Source # (%-) :: forall (t :: Natural) (t :: Natural). Sing t -> Sing t -> Sing (Apply (Apply (-@#@$) t) t) Source # (%*) :: forall (t :: Natural) (t :: Natural). Sing t -> Sing t -> Sing (Apply (Apply (*@#@$) t) t) Source # sNegate :: forall (t :: Natural). Sing t -> Sing (Apply NegateSym0 t) Source # sAbs :: forall (t :: Natural). Sing t -> Sing (Apply AbsSym0 t) Source # sSignum :: forall (t :: Natural). Sing t -> Sing (Apply SignumSym0 t) Source # sFromInteger :: forall (t :: Natural). Sing t -> Sing (Apply FromIntegerSym0 t) Source # | |
| PShow Natural Source # | |
| SShow Natural Source # | |
Defined in Text.Show.Singletons Methods sShowsPrec :: forall (t :: Natural) (t :: Natural) (t :: Symbol). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply ShowsPrecSym0 t) t) t) Source # sShow_ :: forall (t :: Natural). Sing t -> Sing (Apply Show_Sym0 t) Source # sShowList :: forall (t :: [Natural]) (t :: Symbol). Sing t -> Sing t -> Sing (Apply (Apply ShowListSym0 t) t) Source # | |
| KnownNat n => SingI (n :: Nat) | |
Defined in GHC.TypeLits.Singletons.Internal | |
| Lift Natural | |
| SShow a => SingI2 (ShowsPrecSym2 :: Natural -> a -> TyFun Symbol Symbol -> Type) | |
Defined in Text.Show.Singletons Methods liftSing2 :: forall (x :: k1) (y :: k2). Sing x -> Sing y -> Sing (ShowsPrecSym2 x y) | |
| SingI1 DivSym1 | |
Defined in GHC.TypeLits.Singletons | |
| SingI1 ModSym1 | |
Defined in GHC.TypeLits.Singletons | |
| SingI1 (^@#@$$) | |
Defined in GHC.TypeLits.Singletons.Internal | |
| SingI1 (SplitAtSym1 :: Natural -> TyFun (NonEmpty a) ([a], [a]) -> Type) | |
Defined in Data.List.NonEmpty.Singletons Methods liftSing :: forall (x :: k1). Sing x -> Sing (SplitAtSym1 x) | |
| SingI1 (DropSym1 :: Natural -> TyFun (NonEmpty a) [a] -> Type) | |
Defined in Data.List.NonEmpty.Singletons | |
| SingI1 (TakeSym1 :: Natural -> TyFun (NonEmpty a) [a] -> Type) | |
Defined in Data.List.NonEmpty.Singletons | |
| SingI1 (SplitAtSym1 :: Natural -> TyFun [a] ([a], [a]) -> Type) | |
Defined in Data.List.Singletons.Internal Methods liftSing :: forall (x :: k1). Sing x -> Sing (SplitAtSym1 x) | |
| SingI1 (DropSym1 :: Natural -> TyFun [a] [a] -> Type) | |
Defined in Data.List.Singletons.Internal | |
| SingI1 (TakeSym1 :: Natural -> TyFun [a] [a] -> Type) | |
Defined in Data.List.Singletons.Internal | |
| SShow a => SingI1 (ShowsPrecSym1 :: Natural -> TyFun a (Symbol ~> Symbol) -> Type) | |
Defined in Text.Show.Singletons Methods liftSing :: forall (x :: k1). Sing x -> Sing (ShowsPrecSym1 x) | |
| SingI1 (ReplicateSym1 :: Natural -> TyFun a [a] -> Type) | |
Defined in Data.List.Singletons.Internal Methods liftSing :: forall (x :: k1). Sing x -> Sing (ReplicateSym1 x) | |
| SingI1 ((<=?@#@$$) :: Natural -> TyFun Natural Bool -> Type) | |
Defined in GHC.TypeLits.Singletons.Internal Methods liftSing :: forall (x :: k1). Sing x -> Sing ((<=?@#@$$) x) | |
| SEq a => SingI1 (ElemIndexSym1 :: a -> TyFun [a] (Maybe Natural) -> Type) | |
Defined in Data.List.Singletons.Internal Methods liftSing :: forall (x :: k1). Sing x -> Sing (ElemIndexSym1 x) | |
| SEq a => SingI1 (ElemIndicesSym1 :: a -> TyFun [a] [Natural] -> Type) | |
Defined in Data.List.Singletons.Internal Methods liftSing :: forall (x :: k1). Sing x -> Sing (ElemIndicesSym1 x) | |
| SApplicative m => SingI1 (ReplicateM_Sym1 :: Natural -> TyFun (m a) (m ()) -> Type) | |
Defined in Control.Monad.Singletons Methods liftSing :: forall (x :: k1). Sing x -> Sing (ReplicateM_Sym1 x) | |
| SApplicative m => SingI1 (ReplicateMSym1 :: Natural -> TyFun (m a) (m [a]) -> Type) | |
Defined in Control.Monad.Singletons Methods liftSing :: forall (x :: k1). Sing x -> Sing (ReplicateMSym1 x) | |
| SingI1 ((!!@#@$$) :: NonEmpty a -> TyFun Natural a -> Type) | |
Defined in Data.List.NonEmpty.Singletons | |
| SingI1 ((!!@#@$$) :: [a] -> TyFun Natural a -> Type) | |
Defined in Data.List.Singletons.Internal | |
| SingI DivSym0 | |
Defined in GHC.TypeLits.Singletons | |
| SingI ModSym0 | |
Defined in GHC.TypeLits.Singletons | |
| SingI (^@#@$) | |
Defined in GHC.TypeLits.Singletons.Internal | |
| SingI Log2Sym0 | |
Defined in GHC.TypeLits.Singletons | |
| SingI NatToCharSym0 | |
Defined in GHC.TypeLits.Singletons Methods | |
| SingI CharToNatSym0 | |
Defined in GHC.TypeLits.Singletons Methods | |
| SuppressUnusedWarnings KnownNatSym0 Source # | |
Defined in GHC.TypeLits.Singletons Methods suppressUnusedWarnings :: () # | |
| SuppressUnusedWarnings DivSym0 Source # | |
Defined in GHC.TypeLits.Singletons Methods suppressUnusedWarnings :: () # | |
| SuppressUnusedWarnings ModSym0 Source # | |
Defined in GHC.TypeLits.Singletons Methods suppressUnusedWarnings :: () # | |
| SuppressUnusedWarnings QuotSym0 Source # | |
Defined in GHC.TypeLits.Singletons Methods suppressUnusedWarnings :: () # | |
| SuppressUnusedWarnings RemSym0 Source # | |
Defined in GHC.TypeLits.Singletons Methods suppressUnusedWarnings :: () # | |
| SuppressUnusedWarnings (^@#@$) Source # | |
Defined in GHC.TypeLits.Singletons.Internal Methods suppressUnusedWarnings :: () # | |
| SuppressUnusedWarnings DivModSym0 Source # | |
Defined in GHC.TypeLits.Singletons Methods suppressUnusedWarnings :: () # | |
| SuppressUnusedWarnings QuotRemSym0 Source # | |
Defined in GHC.TypeLits.Singletons Methods suppressUnusedWarnings :: () # | |
| SuppressUnusedWarnings Log2Sym0 Source # | |
Defined in GHC.TypeLits.Singletons Methods suppressUnusedWarnings :: () # | |
| SuppressUnusedWarnings NatToCharSym0 Source # | |
Defined in GHC.TypeLits.Singletons Methods suppressUnusedWarnings :: () # | |
| SuppressUnusedWarnings CharToNatSym0 Source # | |
Defined in GHC.TypeLits.Singletons Methods suppressUnusedWarnings :: () # | |
| SingI (FindIndexSym0 :: TyFun (a ~> Bool) ([a] ~> Maybe Natural) -> Type) | |
Defined in Data.List.Singletons.Internal Methods | |
| SingI (FindIndicesSym0 :: TyFun (a ~> Bool) ([a] ~> [Natural]) -> Type) | |
Defined in Data.List.Singletons.Internal Methods | |
| SingI ((!!@#@$) :: TyFun (NonEmpty a) (Natural ~> a) -> Type) | |
Defined in Data.List.NonEmpty.Singletons | |
| SingI (LengthSym0 :: TyFun (NonEmpty a) Natural -> Type) | |
Defined in Data.List.NonEmpty.Singletons Methods sing :: Sing LengthSym0 | |
| SingI (SplitAtSym0 :: TyFun Natural (NonEmpty a ~> ([a], [a])) -> Type) | |
Defined in Data.List.NonEmpty.Singletons Methods sing :: Sing SplitAtSym0 | |
| SingI (DropSym0 :: TyFun Natural (NonEmpty a ~> [a]) -> Type) | |
Defined in Data.List.NonEmpty.Singletons | |
| SingI (TakeSym0 :: TyFun Natural (NonEmpty a ~> [a]) -> Type) | |
Defined in Data.List.NonEmpty.Singletons | |
| SingI (SplitAtSym0 :: TyFun Natural ([a] ~> ([a], [a])) -> Type) | |
Defined in Data.List.Singletons.Internal Methods sing :: Sing SplitAtSym0 | |
| SingI (DropSym0 :: TyFun Natural ([a] ~> [a]) -> Type) | |
Defined in Data.List.Singletons.Internal | |
| SingI (TakeSym0 :: TyFun Natural ([a] ~> [a]) -> Type) | |
Defined in Data.List.Singletons.Internal | |
| SShow a => SingI (ShowsPrecSym0 :: TyFun Natural (a ~> (Symbol ~> Symbol)) -> Type) | |
Defined in Text.Show.Singletons Methods | |
| SingI (ReplicateSym0 :: TyFun Natural (a ~> [a]) -> Type) | |
Defined in Data.List.Singletons.Internal Methods | |
| SEnum a => SingI (ToEnumSym0 :: TyFun Natural a -> Type) | |
Defined in Data.Singletons.Base.Enum Methods sing :: Sing ToEnumSym0 | |
| SNum a => SingI (FromIntegerSym0 :: TyFun Natural a -> Type) | |
Defined in GHC.Num.Singletons Methods | |
| SingI ((!!@#@$) :: TyFun [a] (Natural ~> a) -> Type) | |
Defined in Data.List.Singletons.Internal | |
| SEq a => SingI (ElemIndexSym0 :: TyFun a ([a] ~> Maybe Natural) -> Type) | |
Defined in Data.List.Singletons.Internal Methods | |
| SEq a => SingI (ElemIndicesSym0 :: TyFun a ([a] ~> [Natural]) -> Type) | |
Defined in Data.List.Singletons.Internal Methods | |
| SEnum a => SingI (FromEnumSym0 :: TyFun a Natural -> Type) | |
Defined in Data.Singletons.Base.Enum Methods sing :: Sing FromEnumSym0 | |
| SingI ((<=?@#@$) :: TyFun Natural (Natural ~> Bool) -> Type) | |
Defined in GHC.TypeLits.Singletons.Internal | |
| SingI x => SingI (DivSym1 x :: TyFun Natural Natural -> Type) | |
Defined in GHC.TypeLits.Singletons | |
| SingI x => SingI (ModSym1 x :: TyFun Natural Natural -> Type) | |
Defined in GHC.TypeLits.Singletons | |
| SingI x => SingI ((^@#@$$) x :: TyFun Natural Natural -> Type) | |
Defined in GHC.TypeLits.Singletons.Internal | |
| SuppressUnusedWarnings (FindIndexSym0 :: TyFun (a ~> Bool) ([a] ~> Maybe Natural) -> Type) Source # | |
Defined in Data.List.Singletons.Internal Methods suppressUnusedWarnings :: () # | |
| SuppressUnusedWarnings (FindIndicesSym0 :: TyFun (a ~> Bool) ([a] ~> [Natural]) -> Type) Source # | |
Defined in Data.List.Singletons.Internal Methods suppressUnusedWarnings :: () # | |
| SuppressUnusedWarnings ((!!@#@$) :: TyFun (NonEmpty a) (Natural ~> a) -> Type) Source # | |
Defined in Data.List.NonEmpty.Singletons Methods suppressUnusedWarnings :: () # | |
| SuppressUnusedWarnings (LengthSym0 :: TyFun (NonEmpty a) Natural -> Type) Source # | |
Defined in Data.List.NonEmpty.Singletons Methods suppressUnusedWarnings :: () # | |
| SuppressUnusedWarnings (SplitAtSym0 :: TyFun Natural (NonEmpty a ~> ([a], [a])) -> Type) Source # | |
Defined in Data.List.NonEmpty.Singletons Methods suppressUnusedWarnings :: () # | |
| SuppressUnusedWarnings (DropSym0 :: TyFun Natural (NonEmpty a ~> [a]) -> Type) Source # | |
Defined in Data.List.NonEmpty.Singletons Methods suppressUnusedWarnings :: () # | |
| SuppressUnusedWarnings (TakeSym0 :: TyFun Natural (NonEmpty a ~> [a]) -> Type) Source # | |
Defined in Data.List.NonEmpty.Singletons Methods suppressUnusedWarnings :: () # | |
| SuppressUnusedWarnings (SplitAtSym0 :: TyFun Natural ([a] ~> ([a], [a])) -> Type) Source # | |
Defined in Data.List.Singletons.Internal Methods suppressUnusedWarnings :: () # | |
| SuppressUnusedWarnings (DropSym0 :: TyFun Natural ([a] ~> [a]) -> Type) Source # | |
Defined in Data.List.Singletons.Internal Methods suppressUnusedWarnings :: () # | |
| SuppressUnusedWarnings (TakeSym0 :: TyFun Natural ([a] ~> [a]) -> Type) Source # | |
Defined in Data.List.Singletons.Internal Methods suppressUnusedWarnings :: () # | |
| SuppressUnusedWarnings (ShowsPrecSym0 :: TyFun Natural (a ~> (Symbol ~> Symbol)) -> Type) Source # | |
Defined in Text.Show.Singletons Methods suppressUnusedWarnings :: () # | |
| SuppressUnusedWarnings (ReplicateSym0 :: TyFun Natural (a ~> [a]) -> Type) Source # | |
Defined in Data.List.Singletons.Internal Methods suppressUnusedWarnings :: () # | |
| SuppressUnusedWarnings (DivSym1 a6989586621679558584 :: TyFun Natural Natural -> Type) Source # | |
Defined in GHC.TypeLits.Singletons Methods suppressUnusedWarnings :: () # | |
| SuppressUnusedWarnings (ModSym1 a6989586621679559017 :: TyFun Natural Natural -> Type) Source # | |
Defined in GHC.TypeLits.Singletons Methods suppressUnusedWarnings :: () # | |
| SuppressUnusedWarnings (QuotSym1 a6989586621679559594 :: TyFun Natural Natural -> Type) Source # | |
Defined in GHC.TypeLits.Singletons Methods suppressUnusedWarnings :: () # | |
| SuppressUnusedWarnings (RemSym1 a6989586621679559583 :: TyFun Natural Natural -> Type) Source # | |
Defined in GHC.TypeLits.Singletons Methods suppressUnusedWarnings :: () # | |
| SuppressUnusedWarnings ((^@#@$$) a6989586621679546930 :: TyFun Natural Natural -> Type) Source # | |
Defined in GHC.TypeLits.Singletons.Internal Methods suppressUnusedWarnings :: () # | |
| SuppressUnusedWarnings (DivModSym1 a6989586621679559612 :: TyFun Natural (Natural, Natural) -> Type) Source # | |
Defined in GHC.TypeLits.Singletons Methods suppressUnusedWarnings :: () # | |
| SuppressUnusedWarnings (QuotRemSym1 a6989586621679559605 :: TyFun Natural (Natural, Natural) -> Type) Source # | |
Defined in GHC.TypeLits.Singletons Methods suppressUnusedWarnings :: () # | |
| SuppressUnusedWarnings (ToEnumSym0 :: TyFun Natural a -> Type) Source # | |
Defined in Data.Singletons.Base.Enum Methods suppressUnusedWarnings :: () # | |
| SuppressUnusedWarnings (FromIntegerSym0 :: TyFun Natural a -> Type) Source # | |
Defined in GHC.Num.Singletons Methods suppressUnusedWarnings :: () # | |
| SuppressUnusedWarnings ((!!@#@$) :: TyFun [a] (Natural ~> a) -> Type) Source # | |
Defined in Data.List.Singletons.Internal Methods suppressUnusedWarnings :: () # | |
| SuppressUnusedWarnings (ElemIndexSym0 :: TyFun a ([a] ~> Maybe Natural) -> Type) Source # | |
Defined in Data.List.Singletons.Internal Methods suppressUnusedWarnings :: () # | |
| SuppressUnusedWarnings (ElemIndicesSym0 :: TyFun a ([a] ~> [Natural]) -> Type) Source # | |
Defined in Data.List.Singletons.Internal Methods suppressUnusedWarnings :: () # | |
| SuppressUnusedWarnings (FromEnumSym0 :: TyFun a Natural -> Type) Source # | |
Defined in Data.Singletons.Base.Enum Methods suppressUnusedWarnings :: () # | |
| SApplicative m => SingI (ReplicateM_Sym0 :: TyFun Natural (m a ~> m ()) -> Type) | |
Defined in Control.Monad.Singletons Methods | |
| SApplicative m => SingI (ReplicateMSym0 :: TyFun Natural (m a ~> m [a]) -> Type) | |
Defined in Control.Monad.Singletons Methods | |
| SingI d => SingI ((!!@#@$$) d :: TyFun Natural a -> Type) | |
Defined in Data.List.NonEmpty.Singletons | |
| SingI d => SingI ((!!@#@$$) d :: TyFun Natural a -> Type) | |
Defined in Data.List.Singletons.Internal | |
| (SEq a, SingI d) => SingI (ElemIndexSym1 d :: TyFun [a] (Maybe Natural) -> Type) | |
Defined in Data.List.Singletons.Internal Methods sing :: Sing (ElemIndexSym1 d) | |
| SingI d => SingI (FindIndexSym1 d :: TyFun [a] (Maybe Natural) -> Type) | |
Defined in Data.List.Singletons.Internal Methods sing :: Sing (FindIndexSym1 d) | |
| (SEq a, SingI d) => SingI (ElemIndicesSym1 d :: TyFun [a] [Natural] -> Type) | |
Defined in Data.List.Singletons.Internal Methods sing :: Sing (ElemIndicesSym1 d) | |
| SingI d => SingI (FindIndicesSym1 d :: TyFun [a] [Natural] -> Type) | |
Defined in Data.List.Singletons.Internal Methods sing :: Sing (FindIndicesSym1 d) | |
| SingI x => SingI ((<=?@#@$$) x :: TyFun Natural Bool -> Type) | |
Defined in GHC.TypeLits.Singletons.Internal Methods sing :: Sing ((<=?@#@$$) x) | |
| SuppressUnusedWarnings (ReplicateM_Sym0 :: TyFun Natural (m a ~> m ()) -> Type) Source # | |
Defined in Control.Monad.Singletons Methods suppressUnusedWarnings :: () # | |
| SuppressUnusedWarnings (ReplicateMSym0 :: TyFun Natural (m a ~> m [a]) -> Type) Source # | |
Defined in Control.Monad.Singletons Methods suppressUnusedWarnings :: () # | |
| SuppressUnusedWarnings ((!!@#@$$) a6989586621681170133 :: TyFun Natural a -> Type) Source # | |
Defined in Data.List.NonEmpty.Singletons Methods suppressUnusedWarnings :: () # | |
| SuppressUnusedWarnings ((!!@#@$$) a6989586621679848027 :: TyFun Natural a -> Type) Source # | |
Defined in Data.List.Singletons.Internal Methods suppressUnusedWarnings :: () # | |
| SuppressUnusedWarnings (ElemIndexSym1 a6989586621679848403 :: TyFun [a] (Maybe Natural) -> Type) Source # | |
Defined in Data.List.Singletons.Internal Methods suppressUnusedWarnings :: () # | |
| SuppressUnusedWarnings (FindIndexSym1 a6989586621679848385 :: TyFun [a] (Maybe Natural) -> Type) Source # | |
Defined in Data.List.Singletons.Internal Methods suppressUnusedWarnings :: () # | |
| SuppressUnusedWarnings (ElemIndicesSym1 a6989586621679848394 :: TyFun [a] [Natural] -> Type) Source # | |
Defined in Data.List.Singletons.Internal Methods suppressUnusedWarnings :: () # | |
| SuppressUnusedWarnings (FindIndicesSym1 a6989586621679848362 :: TyFun [a] [Natural] -> Type) Source # | |
Defined in Data.List.Singletons.Internal Methods suppressUnusedWarnings :: () # | |
| SingI1 (FindIndexSym1 :: (a ~> Bool) -> TyFun [a] (Maybe Natural) -> Type) | |
Defined in Data.List.Singletons.Internal Methods liftSing :: forall (x :: k1). Sing x -> Sing (FindIndexSym1 x) | |
| SingI1 (FindIndicesSym1 :: (a ~> Bool) -> TyFun [a] [Natural] -> Type) | |
Defined in Data.List.Singletons.Internal Methods liftSing :: forall (x :: k1). Sing x -> Sing (FindIndicesSym1 x) | |
| SFoldable t => SingI (LengthSym0 :: TyFun (t a) Natural -> Type) | |
Defined in Data.Foldable.Singletons Methods sing :: Sing LengthSym0 | |
| SuppressUnusedWarnings (LengthSym0 :: TyFun (t a) Natural -> Type) Source # | |
Defined in Data.Foldable.Singletons Methods suppressUnusedWarnings :: () # | |
| type Demote Natural | |
Defined in GHC.TypeLits.Singletons.Internal | |
| type Sing Source # | |
Defined in GHC.TypeLits.Singletons.Internal | |
| type FromEnum (a :: Natural) Source # | |
Defined in Data.Singletons.Base.Enum | |
| type Pred (a :: Natural) Source # | |
Defined in Data.Singletons.Base.Enum | |
| type Succ (a :: Natural) Source # | |
Defined in Data.Singletons.Base.Enum | |
| type ToEnum a Source # | |
Defined in Data.Singletons.Base.Enum type ToEnum a | |
| type Abs (a :: Natural) Source # | |
Defined in GHC.Num.Singletons | |
| type FromInteger a Source # | |
Defined in GHC.Num.Singletons type FromInteger a = a | |
| type Negate (a :: Natural) Source # | |
Defined in GHC.Num.Singletons | |
| type Signum (a :: Natural) Source # | |
Defined in GHC.Num.Singletons | |
| type Show_ (arg :: Natural) Source # | |
Defined in Text.Show.Singletons | |
| type Compare (a :: Natural) (b :: Natural) | |
Defined in Data.Type.Ord | |
| type (arg1 :: Natural) /= (arg2 :: Natural) Source # | |
Defined in GHC.TypeLits.Singletons.Internal | |
| type (x :: Natural) == (y :: Natural) Source # | |
Defined in GHC.TypeLits.Singletons.Internal | |
| type (arg1 :: Natural) < (arg2 :: Natural) Source # | |
Defined in GHC.TypeLits.Singletons.Internal | |
| type (arg1 :: Natural) <= (arg2 :: Natural) Source # | |
Defined in GHC.TypeLits.Singletons.Internal | |
| type (arg1 :: Natural) > (arg2 :: Natural) Source # | |
Defined in GHC.TypeLits.Singletons.Internal | |
| type (arg1 :: Natural) >= (arg2 :: Natural) Source # | |
Defined in GHC.TypeLits.Singletons.Internal | |
| type Compare (a :: Natural) (b :: Natural) Source # | |
Defined in GHC.TypeLits.Singletons.Internal | |
| type Max (arg1 :: Natural) (arg2 :: Natural) Source # | |
Defined in GHC.TypeLits.Singletons.Internal | |
| type Min (arg1 :: Natural) (arg2 :: Natural) Source # | |
Defined in GHC.TypeLits.Singletons.Internal | |
| type EnumFromTo (a1 :: Natural) (a2 :: Natural) Source # | |
Defined in Data.Singletons.Base.Enum | |
| type (a :: Natural) * (b :: Natural) Source # | |
Defined in GHC.Num.Singletons | |
| type (a :: Natural) + (b :: Natural) Source # | |
Defined in GHC.Num.Singletons | |
| type (a :: Natural) - (b :: Natural) Source # | |
Defined in GHC.Num.Singletons | |
| type ShowList (arg1 :: [Natural]) arg2 Source # | |
Defined in Text.Show.Singletons | |
| type Apply KnownNatSym0 (a6989586621679557763 :: Nat) | |
Defined in GHC.TypeLits.Singletons | |
| type Apply Log2Sym0 (a6989586621679558354 :: Natural) | |
Defined in GHC.TypeLits.Singletons | |
| type Apply NatToCharSym0 (a6989586621679561676 :: Natural) | |
Defined in GHC.TypeLits.Singletons | |
| type Apply CharToNatSym0 (a6989586621679561453 :: Char) | |
Defined in GHC.TypeLits.Singletons | |
| type EnumFromThenTo (a1 :: Natural) (a2 :: Natural) (a3 :: Natural) Source # | |
Defined in Data.Singletons.Base.Enum | |
| type ShowsPrec _1 (n :: Natural) x Source # | |
Defined in Text.Show.Singletons | |
| type Apply (DivSym1 a6989586621679558584 :: TyFun Natural Natural -> Type) (a6989586621679558585 :: Natural) | |
| type Apply (ModSym1 a6989586621679559017 :: TyFun Natural Natural -> Type) (a6989586621679559018 :: Natural) | |
| type Apply (QuotSym1 a6989586621679559594 :: TyFun Natural Natural -> Type) (a6989586621679559595 :: Natural) | |
| type Apply (RemSym1 a6989586621679559583 :: TyFun Natural Natural -> Type) (a6989586621679559584 :: Natural) | |
| type Apply ((^@#@$$) a6989586621679546930 :: TyFun Natural Natural -> Type) (a6989586621679546931 :: Natural) | |
| type Apply (ToEnumSym0 :: TyFun Natural k2 -> Type) (a6989586621679605385 :: Natural) | |
Defined in Data.Singletons.Base.Enum type Apply (ToEnumSym0 :: TyFun Natural k2 -> Type) (a6989586621679605385 :: Natural) = ToEnum a6989586621679605385 :: k2 | |
| type Apply (FromIntegerSym0 :: TyFun Natural k2 -> Type) (a6989586621679582951 :: Natural) | |
Defined in GHC.Num.Singletons type Apply (FromIntegerSym0 :: TyFun Natural k2 -> Type) (a6989586621679582951 :: Natural) = FromInteger a6989586621679582951 :: k2 | |
| type Apply (FromEnumSym0 :: TyFun a Natural -> Type) (a6989586621679605388 :: a) | |
Defined in Data.Singletons.Base.Enum type Apply (FromEnumSym0 :: TyFun a Natural -> Type) (a6989586621679605388 :: a) = FromEnum a6989586621679605388 | |
| type Apply ((!!@#@$$) a6989586621681170133 :: TyFun Natural a -> Type) (a6989586621681170134 :: Natural) | |
| type Apply ((!!@#@$$) a6989586621679848027 :: TyFun Natural a -> Type) (a6989586621679848028 :: Natural) | |
| type Apply DivSym0 (a6989586621679558584 :: Natural) | |
Defined in GHC.TypeLits.Singletons | |
| type Apply ModSym0 (a6989586621679559017 :: Natural) | |
Defined in GHC.TypeLits.Singletons | |
| type Apply QuotSym0 (a6989586621679559594 :: Natural) | |
Defined in GHC.TypeLits.Singletons | |
| type Apply RemSym0 (a6989586621679559583 :: Natural) | |
Defined in GHC.TypeLits.Singletons | |
| type Apply (^@#@$) (a6989586621679546930 :: Natural) | |
Defined in GHC.TypeLits.Singletons.Internal | |
| type Apply DivModSym0 (a6989586621679559612 :: Natural) | |
Defined in GHC.TypeLits.Singletons | |
| type Apply QuotRemSym0 (a6989586621679559605 :: Natural) | |
Defined in GHC.TypeLits.Singletons | |
| type Apply (SplitAtSym0 :: TyFun Natural (NonEmpty a ~> ([a], [a])) -> Type) (a6989586621681170325 :: Natural) | |
Defined in Data.List.NonEmpty.Singletons type Apply (SplitAtSym0 :: TyFun Natural (NonEmpty a ~> ([a], [a])) -> Type) (a6989586621681170325 :: Natural) = SplitAtSym1 a6989586621681170325 :: TyFun (NonEmpty a) ([a], [a]) -> Type | |
| type Apply (DropSym0 :: TyFun Natural (NonEmpty a ~> [a]) -> Type) (a6989586621681170334 :: Natural) | |
| type Apply (TakeSym0 :: TyFun Natural (NonEmpty a ~> [a]) -> Type) (a6989586621681170343 :: Natural) | |
| type Apply (SplitAtSym0 :: TyFun Natural ([a] ~> ([a], [a])) -> Type) (a6989586621679848182 :: Natural) | |
Defined in Data.List.Singletons.Internal type Apply (SplitAtSym0 :: TyFun Natural ([a] ~> ([a], [a])) -> Type) (a6989586621679848182 :: Natural) = SplitAtSym1 a6989586621679848182 :: TyFun [a] ([a], [a]) -> Type | |
| type Apply (DropSym0 :: TyFun Natural ([a] ~> [a]) -> Type) (a6989586621679848189 :: Natural) | |
| type Apply (TakeSym0 :: TyFun Natural ([a] ~> [a]) -> Type) (a6989586621679848202 :: Natural) | |
| type Apply (ShowsPrecSym0 :: TyFun Natural (a ~> (Symbol ~> Symbol)) -> Type) (a6989586621680243312 :: Natural) | |
Defined in Text.Show.Singletons type Apply (ShowsPrecSym0 :: TyFun Natural (a ~> (Symbol ~> Symbol)) -> Type) (a6989586621680243312 :: Natural) = ShowsPrecSym1 a6989586621680243312 :: TyFun a (Symbol ~> Symbol) -> Type | |
| type Apply (ReplicateSym0 :: TyFun Natural (a ~> [a]) -> Type) (a6989586621679848047 :: Natural) | |
Defined in Data.List.Singletons.Internal type Apply (ReplicateSym0 :: TyFun Natural (a ~> [a]) -> Type) (a6989586621679848047 :: Natural) = ReplicateSym1 a6989586621679848047 :: TyFun a [a] -> Type | |
| type Apply (DivModSym1 a6989586621679559612 :: TyFun Natural (Natural, Natural) -> Type) (a6989586621679559613 :: Natural) | |
Defined in GHC.TypeLits.Singletons | |
| type Apply (QuotRemSym1 a6989586621679559605 :: TyFun Natural (Natural, Natural) -> Type) (a6989586621679559606 :: Natural) | |
Defined in GHC.TypeLits.Singletons | |
| type Apply (ElemIndexSym0 :: TyFun a ([a] ~> Maybe Natural) -> Type) (a6989586621679848403 :: a) | |
Defined in Data.List.Singletons.Internal type Apply (ElemIndexSym0 :: TyFun a ([a] ~> Maybe Natural) -> Type) (a6989586621679848403 :: a) = ElemIndexSym1 a6989586621679848403 | |
| type Apply (ElemIndicesSym0 :: TyFun a ([a] ~> [Natural]) -> Type) (a6989586621679848394 :: a) | |
Defined in Data.List.Singletons.Internal type Apply (ElemIndicesSym0 :: TyFun a ([a] ~> [Natural]) -> Type) (a6989586621679848394 :: a) = ElemIndicesSym1 a6989586621679848394 | |
| type Apply (ReplicateM_Sym0 :: TyFun Natural (m a ~> m ()) -> Type) (a6989586621681332945 :: Natural) | |
Defined in Control.Monad.Singletons type Apply (ReplicateM_Sym0 :: TyFun Natural (m a ~> m ()) -> Type) (a6989586621681332945 :: Natural) = ReplicateM_Sym1 a6989586621681332945 :: TyFun (m a) (m ()) -> Type | |
| type Apply (ReplicateMSym0 :: TyFun Natural (m a ~> m [a]) -> Type) (a6989586621681332963 :: Natural) | |
Defined in Control.Monad.Singletons type Apply (ReplicateMSym0 :: TyFun Natural (m a ~> m [a]) -> Type) (a6989586621681332963 :: Natural) = ReplicateMSym1 a6989586621681332963 :: TyFun (m a) (m [a]) -> Type | |
| type Apply (LengthSym0 :: TyFun (NonEmpty a) Natural -> Type) (a6989586621681170558 :: NonEmpty a) | |
Defined in Data.List.NonEmpty.Singletons | |
| type Apply (LengthSym0 :: TyFun (t a) Natural -> Type) (a6989586621680427282 :: t a) | |
Defined in Data.Foldable.Singletons type Apply (LengthSym0 :: TyFun (t a) Natural -> Type) (a6989586621680427282 :: t a) = Length a6989586621680427282 | |
| type Apply (ElemIndexSym1 a6989586621679848403 :: TyFun [a] (Maybe Natural) -> Type) (a6989586621679848404 :: [a]) | |
Defined in Data.List.Singletons.Internal type Apply (ElemIndexSym1 a6989586621679848403 :: TyFun [a] (Maybe Natural) -> Type) (a6989586621679848404 :: [a]) = ElemIndex a6989586621679848403 a6989586621679848404 | |
| type Apply (FindIndexSym1 a6989586621679848385 :: TyFun [a] (Maybe Natural) -> Type) (a6989586621679848386 :: [a]) | |
Defined in Data.List.Singletons.Internal type Apply (FindIndexSym1 a6989586621679848385 :: TyFun [a] (Maybe Natural) -> Type) (a6989586621679848386 :: [a]) = FindIndex a6989586621679848385 a6989586621679848386 | |
| type Apply (ElemIndicesSym1 a6989586621679848394 :: TyFun [a] [Natural] -> Type) (a6989586621679848395 :: [a]) | |
Defined in Data.List.Singletons.Internal type Apply (ElemIndicesSym1 a6989586621679848394 :: TyFun [a] [Natural] -> Type) (a6989586621679848395 :: [a]) = ElemIndices a6989586621679848394 a6989586621679848395 | |
| type Apply (FindIndicesSym1 a6989586621679848362 :: TyFun [a] [Natural] -> Type) (a6989586621679848363 :: [a]) | |
Defined in Data.List.Singletons.Internal type Apply (FindIndicesSym1 a6989586621679848362 :: TyFun [a] [Natural] -> Type) (a6989586621679848363 :: [a]) = FindIndices a6989586621679848362 a6989586621679848363 | |
| type Apply ((!!@#@$) :: TyFun (NonEmpty a) (Natural ~> a) -> Type) (a6989586621681170133 :: NonEmpty a) | |
| type Apply ((!!@#@$) :: TyFun [a] (Natural ~> a) -> Type) (a6989586621679848027 :: [a]) | |
Defined in Data.List.Singletons.Internal | |
| type Apply (FindIndexSym0 :: TyFun (a ~> Bool) ([a] ~> Maybe Natural) -> Type) (a6989586621679848385 :: a ~> Bool) | |
Defined in Data.List.Singletons.Internal type Apply (FindIndexSym0 :: TyFun (a ~> Bool) ([a] ~> Maybe Natural) -> Type) (a6989586621679848385 :: a ~> Bool) = FindIndexSym1 a6989586621679848385 | |
| type Apply (FindIndicesSym0 :: TyFun (a ~> Bool) ([a] ~> [Natural]) -> Type) (a6989586621679848362 :: a ~> Bool) | |
Defined in Data.List.Singletons.Internal type Apply (FindIndicesSym0 :: TyFun (a ~> Bool) ([a] ~> [Natural]) -> Type) (a6989586621679848362 :: a ~> Bool) = FindIndicesSym1 a6989586621679848362 | |
(Kind) This is the kind of type-level symbols. Declared here because class IP needs it
Instances
The character type Char is an enumeration whose values represent
Unicode (or equivalently ISO/IEC 10646) code points (i.e. characters, see
http://www.unicode.org/ for details). This set extends the ISO 8859-1
(Latin-1) character set (the first 256 characters), which is itself an extension
of the ASCII character set (the first 128 characters). A character literal in
Haskell has type Char.
To convert a Char to or from the corresponding Int value defined
by Unicode, use toEnum and fromEnum from the
Enum class respectively (or equivalently ord and
chr).
Instances
type family Sing :: k -> Type #
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.
withKnownChar :: Sing n -> (KnownChar n => r) -> r Source #
Given a singleton for Char, call something requiring
a KnownChar 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
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 :: forall (n :: Symbol) proxy. KnownSymbol n => proxy n -> String #
Since: base-4.7.0.0
type family (a :: Natural) ^ (b :: Natural) :: Natural where ... infixr 8 #
Exponentiation of type-level naturals.
Since: base-4.7.0.0
type (<=?) (m :: k) (n :: k) = OrdCond (Compare m n) 'True 'True 'False infix 4 #
Comparison (<=) of comparable types, as a function. @since 4.16.0.0
(%<=?) :: forall (a :: Natural) (b :: Natural). Sing a -> Sing b -> Sing (a <=? b) infix 4 Source #
The singleton analogue of <=?
Note that, because of historical reasons in GHC's Natural API, <=?
is incompatible (unification-wise) with <= and the PEq, SEq,
POrd, and SOrd instances for Natural. (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.Ord.Singletons, and not
the <= from GHC.TypeNats. The latter is simply a type alias for
(a .)<=? b) ~ 'True
This is provided here for the sake of completeness and for compatibility
with libraries with APIs built around <=?. New code should use
CmpNat, exposed through this library through the POrd and SOrd
instances for Natural.
type family Log2 (a :: Natural) :: Natural 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 :: Natural) (b :: Natural) :: Natural 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 :: Natural) (b :: Natural) :: Natural 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 DivMod (a :: Natural) (a :: Natural) :: (Natural, Natural) where ... Source #
Equations
| DivMod x y = Apply (Apply Tuple2Sym0 (Apply (Apply DivSym0 x) y)) (Apply (Apply ModSym0 x) y) |
type family QuotRem (a :: Natural) (a :: Natural) :: (Natural, Natural) where ... Source #
Equations
| QuotRem a_6989586621679559598 a_6989586621679559600 = Apply (Apply DivModSym0 a_6989586621679559598) a_6989586621679559600 |
type family ConsSymbol (a :: Char) (b :: Symbol) :: Symbol where ... #
Extending a type-level symbol with a type-level character
Since: base-4.16.0.0
sConsSymbol :: Sing x -> Sing y -> Sing (ConsSymbol x y) Source #
sUnconsSymbol :: Sing x -> Sing (UnconsSymbol x) Source #
type family CharToNat (a :: Char) :: Natural where ... #
Convert a character to its Unicode code point (cf. ord)
Since: base-4.16.0.0
type family NatToChar (a :: Natural) :: Char where ... #
Convert a Unicode code point to a character (cf. chr)
Since: base-4.16.0.0
Defunctionalization symbols
data ErrorSym0 :: (~>) k0 k Source #
Instances
| SingI (ErrorSym0 :: TyFun Symbol a -> Type) Source # | |
Defined in GHC.TypeLits.Singletons.Internal | |
| SuppressUnusedWarnings (ErrorSym0 :: TyFun k0 k -> Type) Source # | |
Defined in GHC.TypeLits.Singletons.Internal Methods suppressUnusedWarnings :: () # | |
| type Apply (ErrorSym0 :: TyFun k0 k2 -> Type) (a6989586621679545715 :: k0) Source # | |
Defined in GHC.TypeLits.Singletons.Internal | |
data ErrorWithoutStackTraceSym0 :: (~>) k0 k Source #
Instances
| SingI (ErrorWithoutStackTraceSym0 :: TyFun Symbol a -> Type) Source # | |
Defined in GHC.TypeLits.Singletons.Internal Methods | |
| SuppressUnusedWarnings (ErrorWithoutStackTraceSym0 :: TyFun k0 k -> Type) Source # | |
Defined in GHC.TypeLits.Singletons.Internal Methods suppressUnusedWarnings :: () # | |
| type Apply (ErrorWithoutStackTraceSym0 :: TyFun k0 k2 -> Type) (a6989586621679545983 :: k0) Source # | |
Defined in GHC.TypeLits.Singletons.Internal type Apply (ErrorWithoutStackTraceSym0 :: TyFun k0 k2 -> Type) (a6989586621679545983 :: k0) = ErrorWithoutStackTrace a6989586621679545983 :: k2 | |
type family ErrorWithoutStackTraceSym1 (a6989586621679545983 :: k0) :: k where ... Source #
Equations
| ErrorWithoutStackTraceSym1 a6989586621679545983 = ErrorWithoutStackTrace a6989586621679545983 |
type family UndefinedSym0 :: k where ... Source #
Equations
| UndefinedSym0 = Undefined |
data KnownNatSym0 :: (~>) Nat Constraint Source #
Instances
| SuppressUnusedWarnings KnownNatSym0 Source # | |
Defined in GHC.TypeLits.Singletons Methods suppressUnusedWarnings :: () # | |
| type Apply KnownNatSym0 (a6989586621679557763 :: Nat) Source # | |
Defined in GHC.TypeLits.Singletons | |
type family KnownNatSym1 (a6989586621679557763 :: Nat) :: Constraint where ... Source #
Equations
| KnownNatSym1 a6989586621679557763 = KnownNat a6989586621679557763 |
data KnownSymbolSym0 :: (~>) Symbol Constraint Source #
Instances
| SuppressUnusedWarnings KnownSymbolSym0 Source # | |
Defined in GHC.TypeLits.Singletons Methods suppressUnusedWarnings :: () # | |
| type Apply KnownSymbolSym0 (a6989586621679557765 :: Symbol) Source # | |
Defined in GHC.TypeLits.Singletons | |
type family KnownSymbolSym1 (a6989586621679557765 :: Symbol) :: Constraint where ... Source #
Equations
| KnownSymbolSym1 a6989586621679557765 = KnownSymbol a6989586621679557765 |
data KnownCharSym0 :: (~>) Char Constraint Source #
Instances
| SuppressUnusedWarnings KnownCharSym0 Source # | |
Defined in GHC.TypeLits.Singletons Methods suppressUnusedWarnings :: () # | |
| type Apply KnownCharSym0 (a6989586621679557767 :: Char) Source # | |
Defined in GHC.TypeLits.Singletons | |
type family KnownCharSym1 (a6989586621679557767 :: Char) :: Constraint where ... Source #
Equations
| KnownCharSym1 a6989586621679557767 = KnownChar a6989586621679557767 |
data (^@#@$) :: (~>) Natural ((~>) Natural Natural) infixr 8 Source #
Instances
| SingI (^@#@$) Source # | |
Defined in GHC.TypeLits.Singletons.Internal | |
| SuppressUnusedWarnings (^@#@$) Source # | |
Defined in GHC.TypeLits.Singletons.Internal Methods suppressUnusedWarnings :: () # | |
| type Apply (^@#@$) (a6989586621679546930 :: Natural) Source # | |
Defined in GHC.TypeLits.Singletons.Internal | |
data (^@#@$$) (a6989586621679546930 :: Natural) :: (~>) Natural Natural infixr 8 Source #
Instances
| SingI1 (^@#@$$) Source # | |
Defined in GHC.TypeLits.Singletons.Internal | |
| SingI x => SingI ((^@#@$$) x :: TyFun Natural Natural -> Type) Source # | |
Defined in GHC.TypeLits.Singletons.Internal | |
| SuppressUnusedWarnings ((^@#@$$) a6989586621679546930 :: TyFun Natural Natural -> Type) Source # | |
Defined in GHC.TypeLits.Singletons.Internal Methods suppressUnusedWarnings :: () # | |
| type Apply ((^@#@$$) a6989586621679546930 :: TyFun Natural Natural -> Type) (a6989586621679546931 :: Natural) Source # | |
type family (a6989586621679546930 :: Natural) ^@#@$$$ (a6989586621679546931 :: Natural) :: Natural where ... infixr 8 Source #
data (<=?@#@$) :: (~>) k ((~>) k Bool) infix 4 Source #
Instances
| SingI ((<=?@#@$) :: TyFun Natural (Natural ~> Bool) -> Type) Source # | |
Defined in GHC.TypeLits.Singletons.Internal | |
| SuppressUnusedWarnings ((<=?@#@$) :: TyFun k (k ~> Bool) -> Type) Source # | |
Defined in GHC.TypeLits.Singletons.Internal Methods suppressUnusedWarnings :: () # | |
| type Apply ((<=?@#@$) :: TyFun k (k ~> Bool) -> Type) (a6989586621679547349 :: k) Source # | |
Defined in GHC.TypeLits.Singletons.Internal type Apply ((<=?@#@$) :: TyFun k (k ~> Bool) -> Type) (a6989586621679547349 :: k) = (<=?@#@$$) a6989586621679547349 | |
data (<=?@#@$$) (a6989586621679547349 :: k) :: (~>) k Bool infix 4 Source #
Instances
| SingI1 ((<=?@#@$$) :: Natural -> TyFun Natural Bool -> Type) Source # | |
Defined in GHC.TypeLits.Singletons.Internal Methods liftSing :: forall (x :: k1). Sing x -> Sing ((<=?@#@$$) x) | |
| SingI x => SingI ((<=?@#@$$) x :: TyFun Natural Bool -> Type) Source # | |
Defined in GHC.TypeLits.Singletons.Internal Methods sing :: Sing ((<=?@#@$$) x) | |
| SuppressUnusedWarnings ((<=?@#@$$) a6989586621679547349 :: TyFun k Bool -> Type) Source # | |
Defined in GHC.TypeLits.Singletons.Internal Methods suppressUnusedWarnings :: () # | |
| type Apply ((<=?@#@$$) a6989586621679547349 :: TyFun k Bool -> Type) (a6989586621679547350 :: k) Source # | |
Defined in GHC.TypeLits.Singletons.Internal type Apply ((<=?@#@$$) a6989586621679547349 :: TyFun k Bool -> Type) (a6989586621679547350 :: k) = a6989586621679547349 <=? a6989586621679547350 | |
type family (a6989586621679547349 :: k) <=?@#@$$$ (a6989586621679547350 :: k) :: Bool where ... infix 4 Source #
data Log2Sym0 :: (~>) Natural Natural Source #
Instances
| SingI Log2Sym0 Source # | |
Defined in GHC.TypeLits.Singletons | |
| SuppressUnusedWarnings Log2Sym0 Source # | |
Defined in GHC.TypeLits.Singletons Methods suppressUnusedWarnings :: () # | |
| type Apply Log2Sym0 (a6989586621679558354 :: Natural) Source # | |
Defined in GHC.TypeLits.Singletons | |
data DivSym0 :: (~>) Natural ((~>) Natural Natural) infixl 7 Source #
Instances
| SingI DivSym0 Source # | |
Defined in GHC.TypeLits.Singletons | |
| SuppressUnusedWarnings DivSym0 Source # | |
Defined in GHC.TypeLits.Singletons Methods suppressUnusedWarnings :: () # | |
| type Apply DivSym0 (a6989586621679558584 :: Natural) Source # | |
Defined in GHC.TypeLits.Singletons | |
data DivSym1 (a6989586621679558584 :: Natural) :: (~>) Natural Natural infixl 7 Source #
Instances
| SingI1 DivSym1 Source # | |
Defined in GHC.TypeLits.Singletons | |
| SingI x => SingI (DivSym1 x :: TyFun Natural Natural -> Type) Source # | |
Defined in GHC.TypeLits.Singletons | |
| SuppressUnusedWarnings (DivSym1 a6989586621679558584 :: TyFun Natural Natural -> Type) Source # | |
Defined in GHC.TypeLits.Singletons Methods suppressUnusedWarnings :: () # | |
| type Apply (DivSym1 a6989586621679558584 :: TyFun Natural Natural -> Type) (a6989586621679558585 :: Natural) Source # | |
type family DivSym2 (a6989586621679558584 :: Natural) (a6989586621679558585 :: Natural) :: Natural where ... infixl 7 Source #
data ModSym0 :: (~>) Natural ((~>) Natural Natural) infixl 7 Source #
Instances
| SingI ModSym0 Source # | |
Defined in GHC.TypeLits.Singletons | |
| SuppressUnusedWarnings ModSym0 Source # | |
Defined in GHC.TypeLits.Singletons Methods suppressUnusedWarnings :: () # | |
| type Apply ModSym0 (a6989586621679559017 :: Natural) Source # | |
Defined in GHC.TypeLits.Singletons | |
data ModSym1 (a6989586621679559017 :: Natural) :: (~>) Natural Natural infixl 7 Source #
Instances
| SingI1 ModSym1 Source # | |
Defined in GHC.TypeLits.Singletons | |
| SingI x => SingI (ModSym1 x :: TyFun Natural Natural -> Type) Source # | |
Defined in GHC.TypeLits.Singletons | |
| SuppressUnusedWarnings (ModSym1 a6989586621679559017 :: TyFun Natural Natural -> Type) Source # | |
Defined in GHC.TypeLits.Singletons Methods suppressUnusedWarnings :: () # | |
| type Apply (ModSym1 a6989586621679559017 :: TyFun Natural Natural -> Type) (a6989586621679559018 :: Natural) Source # | |
type family ModSym2 (a6989586621679559017 :: Natural) (a6989586621679559018 :: Natural) :: Natural where ... infixl 7 Source #
data DivModSym0 :: (~>) Natural ((~>) Natural (Natural, Natural)) Source #
Instances
| SuppressUnusedWarnings DivModSym0 Source # | |
Defined in GHC.TypeLits.Singletons Methods suppressUnusedWarnings :: () # | |
| type Apply DivModSym0 (a6989586621679559612 :: Natural) Source # | |
Defined in GHC.TypeLits.Singletons | |
data DivModSym1 (a6989586621679559612 :: Natural) :: (~>) Natural (Natural, Natural) Source #
Instances
| SuppressUnusedWarnings (DivModSym1 a6989586621679559612 :: TyFun Natural (Natural, Natural) -> Type) Source # | |
Defined in GHC.TypeLits.Singletons Methods suppressUnusedWarnings :: () # | |
| type Apply (DivModSym1 a6989586621679559612 :: TyFun Natural (Natural, Natural) -> Type) (a6989586621679559613 :: Natural) Source # | |
Defined in GHC.TypeLits.Singletons | |
type family DivModSym2 (a6989586621679559612 :: Natural) (a6989586621679559613 :: Natural) :: (Natural, Natural) where ... Source #
Equations
| DivModSym2 a6989586621679559612 a6989586621679559613 = DivMod a6989586621679559612 a6989586621679559613 |
data QuotSym0 :: (~>) Natural ((~>) Natural Natural) infixl 7 Source #
Instances
| SuppressUnusedWarnings QuotSym0 Source # | |
Defined in GHC.TypeLits.Singletons Methods suppressUnusedWarnings :: () # | |
| type Apply QuotSym0 (a6989586621679559594 :: Natural) Source # | |
Defined in GHC.TypeLits.Singletons | |
data QuotSym1 (a6989586621679559594 :: Natural) :: (~>) Natural Natural infixl 7 Source #
type family QuotSym2 (a6989586621679559594 :: Natural) (a6989586621679559595 :: Natural) :: Natural where ... infixl 7 Source #
data RemSym0 :: (~>) Natural ((~>) Natural Natural) infixl 7 Source #
Instances
| SuppressUnusedWarnings RemSym0 Source # | |
Defined in GHC.TypeLits.Singletons Methods suppressUnusedWarnings :: () # | |
| type Apply RemSym0 (a6989586621679559583 :: Natural) Source # | |
Defined in GHC.TypeLits.Singletons | |
data RemSym1 (a6989586621679559583 :: Natural) :: (~>) Natural Natural infixl 7 Source #
type family RemSym2 (a6989586621679559583 :: Natural) (a6989586621679559584 :: Natural) :: Natural where ... infixl 7 Source #
data QuotRemSym0 :: (~>) Natural ((~>) Natural (Natural, Natural)) Source #
Instances
| SuppressUnusedWarnings QuotRemSym0 Source # | |
Defined in GHC.TypeLits.Singletons Methods suppressUnusedWarnings :: () # | |
| type Apply QuotRemSym0 (a6989586621679559605 :: Natural) Source # | |
Defined in GHC.TypeLits.Singletons | |
data QuotRemSym1 (a6989586621679559605 :: Natural) :: (~>) Natural (Natural, Natural) Source #
Instances
| SuppressUnusedWarnings (QuotRemSym1 a6989586621679559605 :: TyFun Natural (Natural, Natural) -> Type) Source # | |
Defined in GHC.TypeLits.Singletons Methods suppressUnusedWarnings :: () # | |
| type Apply (QuotRemSym1 a6989586621679559605 :: TyFun Natural (Natural, Natural) -> Type) (a6989586621679559606 :: Natural) Source # | |
Defined in GHC.TypeLits.Singletons | |
type family QuotRemSym2 (a6989586621679559605 :: Natural) (a6989586621679559606 :: Natural) :: (Natural, Natural) where ... Source #
Equations
| QuotRemSym2 a6989586621679559605 a6989586621679559606 = QuotRem a6989586621679559605 a6989586621679559606 |
data ConsSymbolSym0 :: (~>) Char ((~>) Symbol Symbol) Source #
Instances
| SingI ConsSymbolSym0 Source # | |
Defined in GHC.TypeLits.Singletons Methods | |
| SuppressUnusedWarnings ConsSymbolSym0 Source # | |
Defined in GHC.TypeLits.Singletons Methods suppressUnusedWarnings :: () # | |
| type Apply ConsSymbolSym0 (a6989586621679560776 :: Char) Source # | |
Defined in GHC.TypeLits.Singletons | |
data ConsSymbolSym1 (a6989586621679560776 :: Char) :: (~>) Symbol Symbol Source #
Instances
| SingI1 ConsSymbolSym1 Source # | |
Defined in GHC.TypeLits.Singletons Methods liftSing :: forall (x :: k1). Sing x -> Sing (ConsSymbolSym1 x) | |
| SingI x => SingI (ConsSymbolSym1 x :: TyFun Symbol Symbol -> Type) Source # | |
Defined in GHC.TypeLits.Singletons Methods sing :: Sing (ConsSymbolSym1 x) | |
| SuppressUnusedWarnings (ConsSymbolSym1 a6989586621679560776 :: TyFun Symbol Symbol -> Type) Source # | |
Defined in GHC.TypeLits.Singletons Methods suppressUnusedWarnings :: () # | |
| type Apply (ConsSymbolSym1 a6989586621679560776 :: TyFun Symbol Symbol -> Type) (a6989586621679560777 :: Symbol) Source # | |
Defined in GHC.TypeLits.Singletons type Apply (ConsSymbolSym1 a6989586621679560776 :: TyFun Symbol Symbol -> Type) (a6989586621679560777 :: Symbol) = ConsSymbol a6989586621679560776 a6989586621679560777 | |
type family ConsSymbolSym2 (a6989586621679560776 :: Char) (a6989586621679560777 :: Symbol) :: Symbol where ... Source #
Equations
| ConsSymbolSym2 a6989586621679560776 a6989586621679560777 = ConsSymbol a6989586621679560776 a6989586621679560777 |
data UnconsSymbolSym0 :: (~>) Symbol (Maybe (Char, Symbol)) Source #
Instances
| SingI UnconsSymbolSym0 Source # | |
Defined in GHC.TypeLits.Singletons Methods | |
| SuppressUnusedWarnings UnconsSymbolSym0 Source # | |
Defined in GHC.TypeLits.Singletons Methods suppressUnusedWarnings :: () # | |
| type Apply UnconsSymbolSym0 (a6989586621679561235 :: Symbol) Source # | |
Defined in GHC.TypeLits.Singletons | |
type family UnconsSymbolSym1 (a6989586621679561235 :: Symbol) :: Maybe (Char, Symbol) where ... Source #
Equations
| UnconsSymbolSym1 a6989586621679561235 = UnconsSymbol a6989586621679561235 |
data CharToNatSym0 :: (~>) Char Natural Source #
Instances
| SingI CharToNatSym0 Source # | |
Defined in GHC.TypeLits.Singletons Methods | |
| SuppressUnusedWarnings CharToNatSym0 Source # | |
Defined in GHC.TypeLits.Singletons Methods suppressUnusedWarnings :: () # | |
| type Apply CharToNatSym0 (a6989586621679561453 :: Char) Source # | |
Defined in GHC.TypeLits.Singletons | |
type family CharToNatSym1 (a6989586621679561453 :: Char) :: Natural where ... Source #
Equations
| CharToNatSym1 a6989586621679561453 = CharToNat a6989586621679561453 |
data NatToCharSym0 :: (~>) Natural Char Source #
Instances
| SingI NatToCharSym0 Source # | |
Defined in GHC.TypeLits.Singletons Methods | |
| SuppressUnusedWarnings NatToCharSym0 Source # | |
Defined in GHC.TypeLits.Singletons Methods suppressUnusedWarnings :: () # | |
| type Apply NatToCharSym0 (a6989586621679561676 :: Natural) Source # | |
Defined in GHC.TypeLits.Singletons | |
type family NatToCharSym1 (a6989586621679561676 :: Natural) :: Char where ... Source #
Equations
| NatToCharSym1 a6989586621679561676 = NatToChar a6989586621679561676 |
Orphan instances
| IsString Symbol Source # | |
Methods fromString :: String -> Symbol # | |
| Monoid Symbol Source # | |
| Semigroup Symbol Source # | |
| Show Symbol 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. |
| Ord Symbol Source # | |