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
- type family Sing :: k -> Type
- data SNat (n :: Nat) = KnownNat n => SNat
- data SSymbol (n :: Symbol) = KnownSymbol n => SSym
- 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 :: forall (n :: Nat) proxy. KnownNat n => proxy n -> Natural
- class KnownSymbol (n :: Symbol)
- symbolVal :: forall (n :: Symbol) proxy. KnownSymbol n => proxy n -> String
- type family (a :: Nat) ^ (b :: Nat) :: Nat where ...
- (%^) :: Sing a -> Sing b -> Sing (a ^ b)
- type family (a :: Nat) <=? (b :: Nat) :: Bool where ...
- (%<=?) :: Sing a -> Sing b -> Sing (a <=? b)
- type family Log2 (a :: Nat) :: Nat where ...
- sLog2 :: Sing x -> Sing (Log2 x)
- type family Div (a :: Nat) (b :: Nat) :: Nat where ...
- sDiv :: Sing x -> Sing y -> Sing (Div x y)
- type family Mod (a :: Nat) (b :: Nat) :: Nat where ...
- sMod :: Sing x -> Sing y -> Sing (Mod x y)
- type family DivMod (a :: 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 k06989586621679481870 k6989586621679481871. (~>) k06989586621679481870 k6989586621679481871
- type ErrorSym1 (str6989586621679481872 :: k06989586621679481870) = Error str6989586621679481872
- data ErrorWithoutStackTraceSym0 :: forall k06989586621679482960 k6989586621679482961. (~>) k06989586621679482960 k6989586621679482961
- type ErrorWithoutStackTraceSym1 (str6989586621679482962 :: k06989586621679482960) = ErrorWithoutStackTrace str6989586621679482962
- type UndefinedSym0 = Undefined
- data KnownNatSym0 :: (~>) Nat Constraint
- type KnownNatSym1 (n6989586621679482027 :: Nat) = KnownNat n6989586621679482027
- data KnownSymbolSym0 :: (~>) Symbol Constraint
- type KnownSymbolSym1 (n6989586621679482093 :: Symbol) = KnownSymbol n6989586621679482093
- 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 (a6989586621679504167 :: Nat) :: (~>) Nat (Nat, Nat)
- type DivModSym2 (a6989586621679504167 :: Nat) (a6989586621679504168 :: Nat) = DivMod a6989586621679504167 a6989586621679504168
- data QuotSym0 :: (~>) Nat ((~>) Nat Nat)
- data QuotSym1 (a6989586621679504151 :: Nat) :: (~>) Nat Nat
- type QuotSym2 (a6989586621679504151 :: Nat) (a6989586621679504152 :: Nat) = Quot a6989586621679504151 a6989586621679504152
- data RemSym0 :: (~>) Nat ((~>) Nat Nat)
- data RemSym1 (a6989586621679504141 :: Nat) :: (~>) Nat Nat
- type RemSym2 (a6989586621679504141 :: Nat) (a6989586621679504142 :: Nat) = Rem a6989586621679504141 a6989586621679504142
- data QuotRemSym0 :: (~>) Nat ((~>) Nat (Nat, Nat))
- data QuotRemSym1 (a6989586621679504161 :: Nat) :: (~>) Nat (Nat, Nat)
- type QuotRemSym2 (a6989586621679504161 :: Nat) (a6989586621679504162 :: Nat) = QuotRem a6989586621679504161 a6989586621679504162
Documentation
Instances
Enum Nat | |
Eq Nat | |
Num Nat | This bogus |
Ord Nat | |
Show Nat | |
SingKind Nat Source # | |
SDecide Nat Source # | |
PEq Nat Source # | |
SEq Nat Source # | |
SOrd Nat Source # | |
Defined in Data.Singletons.TypeLits.Internal Methods sCompare :: forall (t :: Nat) (t :: Nat). Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source # (%<) :: forall (t :: Nat) (t :: Nat). Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source # (%<=) :: forall (t :: Nat) (t :: Nat). Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source # (%>) :: forall (t :: Nat) (t :: Nat). Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source # (%>=) :: forall (t :: Nat) (t :: Nat). Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source # sMax :: forall (t :: Nat) (t :: Nat). Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source # sMin :: forall (t :: Nat) (t :: Nat). Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source # | |
POrd Nat Source # | |
SNum Nat Source # | |
Defined in Data.Singletons.Prelude.Num Methods (%+) :: forall (t :: Nat) (t :: Nat). Sing t -> Sing t -> Sing (Apply (Apply (+@#@$) t) t) Source # (%-) :: forall (t :: Nat) (t :: Nat). Sing t -> Sing t -> Sing (Apply (Apply (-@#@$) t) t) Source # (%*) :: forall (t :: Nat) (t :: Nat). Sing t -> Sing t -> Sing (Apply (Apply (*@#@$) t) t) Source # sNegate :: forall (t :: Nat). Sing t -> Sing (Apply NegateSym0 t) Source # sAbs :: forall (t :: Nat). Sing t -> Sing (Apply AbsSym0 t) Source # sSignum :: forall (t :: Nat). Sing t -> Sing (Apply SignumSym0 t) Source # sFromInteger :: forall (t :: Nat). Sing t -> Sing (Apply FromIntegerSym0 t) Source # | |
PNum Nat Source # | |
SEnum Nat Source # | |
Defined in Data.Singletons.Prelude.Enum Methods sSucc :: forall (t :: Nat). Sing t -> Sing (Apply SuccSym0 t) Source # sPred :: forall (t :: Nat). Sing t -> Sing (Apply PredSym0 t) Source # sToEnum :: forall (t :: Nat). Sing t -> Sing (Apply ToEnumSym0 t) Source # sFromEnum :: forall (t :: Nat). Sing t -> Sing (Apply FromEnumSym0 t) Source # sEnumFromTo :: forall (t :: Nat) (t :: Nat). Sing t -> Sing t -> Sing (Apply (Apply EnumFromToSym0 t) t) Source # sEnumFromThenTo :: forall (t :: Nat) (t :: Nat) (t :: Nat). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply EnumFromThenToSym0 t) t) t) Source # | |
PEnum Nat Source # | |
SShow Nat Source # | |
Defined in Data.Singletons.Prelude.Show Methods sShowsPrec :: forall (t :: Nat) (t :: Nat) (t :: Symbol). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply ShowsPrecSym0 t) t) t) Source # sShow_ :: forall (t :: Nat). Sing t -> Sing (Apply Show_Sym0 t) Source # sShowList :: forall (t :: [Nat]) (t :: Symbol). Sing t -> Sing t -> Sing (Apply (Apply ShowListSym0 t) t) Source # | |
PShow Nat Source # | |
KnownNat n => SingI (n :: Nat) Source # | |
Defined in Data.Singletons.TypeLits.Internal | |
SingI Log2Sym0 Source # | |
SingI (<=?@#@$) Source # | |
SingI (^@#@$) Source # | |
SingI DivSym0 Source # | |
SingI ModSym0 Source # | |
SuppressUnusedWarnings KnownNatSym0 Source # | |
Defined in Data.Singletons.TypeLits Methods suppressUnusedWarnings :: () Source # | |
SuppressUnusedWarnings Log2Sym0 Source # | |
Defined in Data.Singletons.TypeLits Methods suppressUnusedWarnings :: () Source # | |
SuppressUnusedWarnings (<=?@#@$) Source # | |
Defined in Data.Singletons.TypeLits.Internal Methods suppressUnusedWarnings :: () Source # | |
SuppressUnusedWarnings (^@#@$) Source # | |
Defined in Data.Singletons.TypeLits.Internal Methods suppressUnusedWarnings :: () Source # | |
SuppressUnusedWarnings DivSym0 Source # | |
Defined in Data.Singletons.TypeLits Methods suppressUnusedWarnings :: () Source # | |
SuppressUnusedWarnings ModSym0 Source # | |
Defined in Data.Singletons.TypeLits Methods suppressUnusedWarnings :: () Source # | |
SuppressUnusedWarnings QuotSym0 Source # | |
Defined in Data.Singletons.TypeLits Methods suppressUnusedWarnings :: () Source # | |
SuppressUnusedWarnings RemSym0 Source # | |
Defined in Data.Singletons.TypeLits Methods suppressUnusedWarnings :: () Source # | |
SuppressUnusedWarnings DivModSym0 Source # | |
Defined in Data.Singletons.TypeLits Methods suppressUnusedWarnings :: () Source # | |
SuppressUnusedWarnings QuotRemSym0 Source # | |
Defined in Data.Singletons.TypeLits Methods suppressUnusedWarnings :: () Source # | |
SingI x => SingI ((<=?@#@$$) x :: TyFun Nat Bool -> Type) Source # | |
Defined in Data.Singletons.TypeLits.Internal Methods sing :: Sing ((<=?@#@$$) x) Source # | |
SingI x => SingI ((^@#@$$) x :: TyFun Nat Nat -> Type) Source # | |
SingI x => SingI (DivSym1 x :: TyFun Nat Nat -> Type) Source # | |
SingI x => SingI (ModSym1 x :: TyFun Nat Nat -> Type) Source # | |
SingI ((!!@#@$) :: TyFun [a] (Nat ~> a) -> Type) Source # | |
SNum a => SingI (FromIntegerSym0 :: TyFun Nat a -> Type) Source # | |
Defined in Data.Singletons.Prelude.Num Methods | |
SEnum a => SingI (ToEnumSym0 :: TyFun Nat a -> Type) Source # | |
Defined in Data.Singletons.Prelude.Enum Methods sing :: Sing ToEnumSym0 Source # | |
SingI (SplitAtSym0 :: TyFun Nat ([a] ~> ([a], [a])) -> Type) Source # | |
Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing SplitAtSym0 Source # | |
SingI (DropSym0 :: TyFun Nat ([a] ~> [a]) -> Type) Source # | |
SingI (TakeSym0 :: TyFun Nat ([a] ~> [a]) -> Type) Source # | |
SingI (ReplicateSym0 :: TyFun Nat (a ~> [a]) -> Type) Source # | |
Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing ReplicateSym0 Source # | |
SShow a => SingI (ShowsPrecSym0 :: TyFun Nat (a ~> (Symbol ~> Symbol)) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Show Methods sing :: Sing ShowsPrecSym0 Source # | |
SingI (SplitAtSym0 :: TyFun Nat (NonEmpty a ~> ([a], [a])) -> Type) Source # | |
Defined in Data.Singletons.Prelude.List.NonEmpty Methods sing :: Sing SplitAtSym0 Source # | |
SingI (DropSym0 :: TyFun Nat (NonEmpty a ~> [a]) -> Type) Source # | |
SingI (TakeSym0 :: TyFun Nat (NonEmpty a ~> [a]) -> Type) Source # | |
SEnum a => SingI (FromEnumSym0 :: TyFun a Nat -> Type) Source # | |
Defined in Data.Singletons.Prelude.Enum Methods sing :: Sing FromEnumSym0 Source # | |
SEq a => SingI (ElemIndicesSym0 :: TyFun a ([a] ~> [Nat]) -> Type) Source # | |
Defined in Data.Singletons.Prelude.List.Internal Methods | |
SEq a => SingI (ElemIndexSym0 :: TyFun a ([a] ~> Maybe Nat) -> Type) Source # | |
Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing ElemIndexSym0 Source # | |
SingI ((!!@#@$) :: TyFun (NonEmpty a) (Nat ~> a) -> Type) Source # | |
SingI (LengthSym0 :: TyFun (NonEmpty a) Nat -> Type) Source # | |
Defined in Data.Singletons.Prelude.List.NonEmpty Methods sing :: Sing LengthSym0 Source # | |
SingI (FindIndicesSym0 :: TyFun (a ~> Bool) ([a] ~> [Nat]) -> Type) Source # | |
Defined in Data.Singletons.Prelude.List.Internal Methods | |
SingI (FindIndexSym0 :: TyFun (a ~> Bool) ([a] ~> Maybe Nat) -> Type) Source # | |
Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing FindIndexSym0 Source # | |
SuppressUnusedWarnings ((!!@#@$) :: TyFun [a6989586621679970139] (Nat ~> a6989586621679970139) -> Type) Source # | |
Defined in Data.Singletons.Prelude.List.Internal Methods suppressUnusedWarnings :: () Source # | |
SuppressUnusedWarnings ((<=?@#@$$) a3530822107858468865 :: TyFun Nat Bool -> Type) Source # | |
Defined in Data.Singletons.TypeLits.Internal Methods suppressUnusedWarnings :: () Source # | |
SuppressUnusedWarnings ((^@#@$$) a3530822107858468865 :: TyFun Nat Nat -> Type) Source # | |
Defined in Data.Singletons.TypeLits.Internal Methods suppressUnusedWarnings :: () Source # | |
SuppressUnusedWarnings (DivSym1 a3530822107858468865 :: TyFun Nat Nat -> Type) Source # | |
Defined in Data.Singletons.TypeLits Methods suppressUnusedWarnings :: () Source # | |
SuppressUnusedWarnings (ModSym1 a3530822107858468865 :: TyFun Nat Nat -> Type) Source # | |
Defined in Data.Singletons.TypeLits Methods suppressUnusedWarnings :: () Source # | |
SuppressUnusedWarnings (QuotSym1 a6989586621679504151 :: TyFun Nat Nat -> Type) Source # | |
Defined in Data.Singletons.TypeLits Methods suppressUnusedWarnings :: () Source # | |
SuppressUnusedWarnings (RemSym1 a6989586621679504141 :: TyFun Nat Nat -> Type) Source # | |
Defined in Data.Singletons.TypeLits Methods suppressUnusedWarnings :: () Source # | |
SuppressUnusedWarnings (DivModSym1 a6989586621679504167 :: TyFun Nat (Nat, Nat) -> Type) Source # | |
Defined in Data.Singletons.TypeLits Methods suppressUnusedWarnings :: () Source # | |
SuppressUnusedWarnings (QuotRemSym1 a6989586621679504161 :: TyFun Nat (Nat, Nat) -> Type) Source # | |
Defined in Data.Singletons.TypeLits Methods suppressUnusedWarnings :: () Source # | |
SuppressUnusedWarnings (FromIntegerSym0 :: TyFun Nat a6989586621679525420 -> Type) Source # | |
Defined in Data.Singletons.Prelude.Num Methods suppressUnusedWarnings :: () Source # | |
SuppressUnusedWarnings (ToEnumSym0 :: TyFun Nat a6989586621679763112 -> Type) Source # | |
Defined in Data.Singletons.Prelude.Enum Methods suppressUnusedWarnings :: () Source # | |
SuppressUnusedWarnings (DropSym0 :: TyFun Nat ([a6989586621679970156] ~> [a6989586621679970156]) -> Type) Source # | |
Defined in Data.Singletons.Prelude.List.Internal Methods suppressUnusedWarnings :: () Source # | |
SuppressUnusedWarnings (TakeSym0 :: TyFun Nat ([a6989586621679970157] ~> [a6989586621679970157]) -> Type) Source # | |
Defined in Data.Singletons.Prelude.List.Internal Methods suppressUnusedWarnings :: () Source # | |
SuppressUnusedWarnings (SplitAtSym0 :: TyFun Nat ([a6989586621679970155] ~> ([a6989586621679970155], [a6989586621679970155])) -> Type) Source # | |
Defined in Data.Singletons.Prelude.List.Internal Methods suppressUnusedWarnings :: () Source # | |
SuppressUnusedWarnings (ReplicateSym0 :: TyFun Nat (a6989586621679970141 ~> [a6989586621679970141]) -> Type) Source # | |
Defined in Data.Singletons.Prelude.List.Internal Methods suppressUnusedWarnings :: () Source # | |
SuppressUnusedWarnings (ShowsPrecSym0 :: TyFun Nat (a6989586621680290698 ~> (Symbol ~> Symbol)) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Show Methods suppressUnusedWarnings :: () Source # | |
SuppressUnusedWarnings (TakeSym0 :: TyFun Nat (NonEmpty a6989586621681159612 ~> [a6989586621681159612]) -> Type) Source # | |
Defined in Data.Singletons.Prelude.List.NonEmpty Methods suppressUnusedWarnings :: () Source # | |
SuppressUnusedWarnings (DropSym0 :: TyFun Nat (NonEmpty a6989586621681159611 ~> [a6989586621681159611]) -> Type) Source # | |
Defined in Data.Singletons.Prelude.List.NonEmpty Methods suppressUnusedWarnings :: () Source # | |
SuppressUnusedWarnings (SplitAtSym0 :: TyFun Nat (NonEmpty a6989586621681159610 ~> ([a6989586621681159610], [a6989586621681159610])) -> Type) Source # | |
Defined in Data.Singletons.Prelude.List.NonEmpty Methods suppressUnusedWarnings :: () Source # | |
SuppressUnusedWarnings (FromEnumSym0 :: TyFun a6989586621679763112 Nat -> Type) Source # | |
Defined in Data.Singletons.Prelude.Enum Methods suppressUnusedWarnings :: () Source # | |
SuppressUnusedWarnings (ElemIndicesSym0 :: TyFun a6989586621679970167 ([a6989586621679970167] ~> [Nat]) -> Type) Source # | |
Defined in Data.Singletons.Prelude.List.Internal Methods suppressUnusedWarnings :: () Source # | |
SuppressUnusedWarnings (ElemIndexSym0 :: TyFun a6989586621679970168 ([a6989586621679970168] ~> Maybe Nat) -> Type) Source # | |
Defined in Data.Singletons.Prelude.List.Internal Methods suppressUnusedWarnings :: () Source # | |
SuppressUnusedWarnings ((!!@#@$) :: TyFun (NonEmpty a6989586621681159590) (Nat ~> a6989586621681159590) -> Type) Source # | |
Defined in Data.Singletons.Prelude.List.NonEmpty Methods suppressUnusedWarnings :: () Source # | |
SuppressUnusedWarnings (LengthSym0 :: TyFun (NonEmpty a6989586621681159643) Nat -> Type) Source # | |
Defined in Data.Singletons.Prelude.List.NonEmpty Methods suppressUnusedWarnings :: () Source # | |
SuppressUnusedWarnings (FindIndicesSym0 :: TyFun (a6989586621679970165 ~> Bool) ([a6989586621679970165] ~> [Nat]) -> Type) Source # | |
Defined in Data.Singletons.Prelude.List.Internal Methods suppressUnusedWarnings :: () Source # | |
SuppressUnusedWarnings (FindIndexSym0 :: TyFun (a6989586621679970166 ~> Bool) ([a6989586621679970166] ~> Maybe Nat) -> Type) Source # | |
Defined in Data.Singletons.Prelude.List.Internal Methods suppressUnusedWarnings :: () Source # | |
SingI d => SingI (FindIndicesSym1 d :: TyFun [a] [Nat] -> Type) Source # | |
Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (FindIndicesSym1 d) Source # | |
SingI d => SingI (FindIndexSym1 d :: TyFun [a] (Maybe Nat) -> Type) Source # | |
Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (FindIndexSym1 d) Source # | |
(SEq a, SingI d) => SingI (ElemIndicesSym1 d :: TyFun [a] [Nat] -> Type) Source # | |
Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (ElemIndicesSym1 d) Source # | |
(SEq a, SingI d) => SingI (ElemIndexSym1 d :: TyFun [a] (Maybe Nat) -> Type) Source # | |
Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (ElemIndexSym1 d) Source # | |
SingI d => SingI ((!!@#@$$) d :: TyFun Nat a -> Type) Source # | |
SingI d => SingI ((!!@#@$$) d :: TyFun Nat a -> Type) Source # | |
SApplicative m => SingI (ReplicateM_Sym0 :: TyFun Nat (m a ~> m ()) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Monad Methods | |
SApplicative m => SingI (ReplicateMSym0 :: TyFun Nat (m a ~> m [a]) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Monad Methods | |
SuppressUnusedWarnings (FindIndicesSym1 a6989586621679974667 :: TyFun [a6989586621679970165] [Nat] -> Type) Source # | |
Defined in Data.Singletons.Prelude.List.Internal Methods suppressUnusedWarnings :: () Source # | |
SuppressUnusedWarnings (ElemIndicesSym1 a6989586621679974701 :: TyFun [a6989586621679970167] [Nat] -> Type) Source # | |
Defined in Data.Singletons.Prelude.List.Internal Methods suppressUnusedWarnings :: () Source # | |
SuppressUnusedWarnings (FindIndexSym1 a6989586621679974693 :: TyFun [a6989586621679970166] (Maybe Nat) -> Type) Source # | |
Defined in Data.Singletons.Prelude.List.Internal Methods suppressUnusedWarnings :: () Source # | |
SuppressUnusedWarnings (ElemIndexSym1 a6989586621679974709 :: TyFun [a6989586621679970168] (Maybe Nat) -> Type) Source # | |
Defined in Data.Singletons.Prelude.List.Internal Methods suppressUnusedWarnings :: () Source # | |
SuppressUnusedWarnings ((!!@#@$$) a6989586621679974286 :: TyFun Nat a6989586621679970139 -> Type) Source # | |
Defined in Data.Singletons.Prelude.List.Internal Methods suppressUnusedWarnings :: () Source # | |
SuppressUnusedWarnings ((!!@#@$$) a6989586621681160950 :: TyFun Nat a6989586621681159590 -> Type) Source # | |
Defined in Data.Singletons.Prelude.List.NonEmpty Methods suppressUnusedWarnings :: () Source # | |
SuppressUnusedWarnings (ReplicateM_Sym0 :: TyFun Nat (m6989586621681270963 a6989586621681270964 ~> m6989586621681270963 ()) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Monad Methods suppressUnusedWarnings :: () Source # | |
SuppressUnusedWarnings (ReplicateMSym0 :: TyFun Nat (m6989586621681270965 a6989586621681270966 ~> m6989586621681270965 [a6989586621681270966]) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Monad Methods suppressUnusedWarnings :: () Source # | |
SFoldable t => SingI (LengthSym0 :: TyFun (t a) Nat -> Type) Source # | |
Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing LengthSym0 Source # | |
SuppressUnusedWarnings (LengthSym0 :: TyFun (t6989586621680486579 a6989586621680486595) Nat -> Type) Source # | |
Defined in Data.Singletons.Prelude.Foldable Methods suppressUnusedWarnings :: () Source # | |
type Demote Nat Source # | |
Defined in Data.Singletons.TypeLits.Internal | |
type Sing Source # | |
Defined in Data.Singletons.TypeLits.Internal | |
type Negate (a :: Nat) Source # | |
Defined in Data.Singletons.Prelude.Num | |
type Abs (a :: Nat) Source # | |
Defined in Data.Singletons.Prelude.Num | |
type Signum (a :: Nat) Source # | |
Defined in Data.Singletons.Prelude.Num | |
type FromInteger a Source # | |
Defined in Data.Singletons.Prelude.Num type FromInteger a = a | |
type Succ (a :: Nat) Source # | |
Defined in Data.Singletons.Prelude.Enum | |
type Pred (a :: Nat) Source # | |
Defined in Data.Singletons.Prelude.Enum | |
type ToEnum a Source # | |
Defined in Data.Singletons.Prelude.Enum type ToEnum a | |
type FromEnum (a :: Nat) Source # | |
Defined in Data.Singletons.Prelude.Enum | |
type Show_ (arg0 :: Nat) Source # | |
Defined in Data.Singletons.Prelude.Show | |
type (x :: Nat) == (y :: Nat) Source # | |
Defined in Data.Singletons.TypeLits.Internal | |
type (x :: Nat) /= (y :: Nat) Source # | |
type Compare (a :: Nat) (b :: Nat) Source # | |
Defined in Data.Singletons.TypeLits.Internal | |
type (arg1 :: Nat) < (arg2 :: Nat) Source # | |
Defined in Data.Singletons.TypeLits.Internal | |
type (arg1 :: Nat) <= (arg2 :: Nat) Source # | |
Defined in Data.Singletons.TypeLits.Internal | |
type (arg1 :: Nat) > (arg2 :: Nat) Source # | |
Defined in Data.Singletons.TypeLits.Internal | |
type (arg1 :: Nat) >= (arg2 :: Nat) Source # | |
Defined in Data.Singletons.TypeLits.Internal | |
type Max (arg1 :: Nat) (arg2 :: Nat) Source # | |
Defined in Data.Singletons.TypeLits.Internal | |
type Min (arg1 :: Nat) (arg2 :: Nat) Source # | |
Defined in Data.Singletons.TypeLits.Internal | |
type (a :: Nat) + (b :: Nat) Source # | |
Defined in Data.Singletons.Prelude.Num | |
type (a :: Nat) - (b :: Nat) Source # | |
Defined in Data.Singletons.Prelude.Num | |
type (a :: Nat) * (b :: Nat) Source # | |
Defined in Data.Singletons.Prelude.Num | |
type EnumFromTo (a1 :: Nat) (a2 :: Nat) Source # | |
Defined in Data.Singletons.Prelude.Enum | |
type ShowList (arg1 :: [Nat]) arg2 Source # | |
Defined in Data.Singletons.Prelude.Show | |
type Apply KnownNatSym0 (n6989586621679482027 :: Nat) Source # | |
Defined in Data.Singletons.TypeLits | |
type Apply Log2Sym0 (a3530822107858468865 :: Nat) Source # | |
Defined in Data.Singletons.TypeLits | |
type EnumFromThenTo (a1 :: Nat) (a2 :: Nat) (a3 :: Nat) Source # | |
Defined in Data.Singletons.Prelude.Enum | |
type ShowsPrec _1 (n :: Nat) x Source # | |
Defined in Data.Singletons.Prelude.Show | |
type Apply ((<=?@#@$$) a3530822107858468865 :: TyFun Nat Bool -> Type) (b3530822107858468866 :: Nat) Source # | |
Defined in Data.Singletons.TypeLits.Internal | |
type Apply ((^@#@$$) a3530822107858468865 :: TyFun Nat Nat -> Type) (b3530822107858468866 :: Nat) Source # | |
type Apply (DivSym1 a3530822107858468865 :: TyFun Nat Nat -> Type) (b3530822107858468866 :: Nat) Source # | |
type Apply (ModSym1 a3530822107858468865 :: TyFun Nat Nat -> Type) (b3530822107858468866 :: Nat) Source # | |
type Apply (QuotSym1 a6989586621679504151 :: TyFun Nat Nat -> Type) (a6989586621679504152 :: Nat) Source # | |
type Apply (RemSym1 a6989586621679504141 :: TyFun Nat Nat -> Type) (a6989586621679504142 :: Nat) Source # | |
type Apply (FromIntegerSym0 :: TyFun Nat k2 -> Type) (arg6989586621679525457 :: Nat) Source # | |
Defined in Data.Singletons.Prelude.Num type Apply (FromIntegerSym0 :: TyFun Nat k2 -> Type) (arg6989586621679525457 :: Nat) = FromInteger arg6989586621679525457 :: k2 | |
type Apply (ToEnumSym0 :: TyFun Nat k2 -> Type) (arg6989586621679763400 :: Nat) Source # | |
Defined in Data.Singletons.Prelude.Enum | |
type Apply (FromEnumSym0 :: TyFun a Nat -> Type) (arg6989586621679763402 :: a) Source # | |
Defined in Data.Singletons.Prelude.Enum type Apply (FromEnumSym0 :: TyFun a Nat -> Type) (arg6989586621679763402 :: a) = FromEnum arg6989586621679763402 | |
type Apply ((!!@#@$$) a6989586621679974286 :: TyFun Nat a -> Type) (a6989586621679974287 :: Nat) Source # | |
type Apply ((!!@#@$$) a6989586621681160950 :: TyFun Nat a -> Type) (a6989586621681160951 :: Nat) Source # | |
type Apply (<=?@#@$) (a3530822107858468865 :: Nat) Source # | |
Defined in Data.Singletons.TypeLits.Internal | |
type Apply (^@#@$) (a3530822107858468865 :: Nat) Source # | |
Defined in Data.Singletons.TypeLits.Internal | |
type Apply DivSym0 (a3530822107858468865 :: Nat) Source # | |
Defined in Data.Singletons.TypeLits | |
type Apply ModSym0 (a3530822107858468865 :: Nat) Source # | |
Defined in Data.Singletons.TypeLits | |
type Apply QuotSym0 (a6989586621679504151 :: Nat) Source # | |
Defined in Data.Singletons.TypeLits | |
type Apply RemSym0 (a6989586621679504141 :: Nat) Source # | |
Defined in Data.Singletons.TypeLits | |
type Apply DivModSym0 (a6989586621679504167 :: Nat) Source # | |
Defined in Data.Singletons.TypeLits | |
type Apply QuotRemSym0 (a6989586621679504161 :: Nat) Source # | |
Defined in Data.Singletons.TypeLits | |
type Apply (DivModSym1 a6989586621679504167 :: TyFun Nat (Nat, Nat) -> Type) (a6989586621679504168 :: Nat) Source # | |
Defined in Data.Singletons.TypeLits | |
type Apply (QuotRemSym1 a6989586621679504161 :: TyFun Nat (Nat, Nat) -> Type) (a6989586621679504162 :: Nat) Source # | |
Defined in Data.Singletons.TypeLits | |
type Apply (DropSym0 :: TyFun Nat ([a6989586621679970156] ~> [a6989586621679970156]) -> Type) (a6989586621679974453 :: Nat) Source # | |
type Apply (TakeSym0 :: TyFun Nat ([a6989586621679970157] ~> [a6989586621679970157]) -> Type) (a6989586621679974467 :: Nat) Source # | |
type Apply (SplitAtSym0 :: TyFun Nat ([a6989586621679970155] ~> ([a6989586621679970155], [a6989586621679970155])) -> Type) (a6989586621679974447 :: Nat) Source # | |
Defined in Data.Singletons.Prelude.List.Internal type Apply (SplitAtSym0 :: TyFun Nat ([a6989586621679970155] ~> ([a6989586621679970155], [a6989586621679970155])) -> Type) (a6989586621679974447 :: Nat) = SplitAtSym1 a6989586621679974447 a6989586621679970155 :: TyFun [a6989586621679970155] ([a6989586621679970155], [a6989586621679970155]) -> Type | |
type Apply (ReplicateSym0 :: TyFun Nat (a6989586621679970141 ~> [a6989586621679970141]) -> Type) (a6989586621679974306 :: Nat) Source # | |
Defined in Data.Singletons.Prelude.List.Internal type Apply (ReplicateSym0 :: TyFun Nat (a6989586621679970141 ~> [a6989586621679970141]) -> Type) (a6989586621679974306 :: Nat) = ReplicateSym1 a6989586621679974306 a6989586621679970141 :: TyFun a6989586621679970141 [a6989586621679970141] -> Type | |
type Apply (ShowsPrecSym0 :: TyFun Nat (a6989586621680290698 ~> (Symbol ~> Symbol)) -> Type) (arg6989586621680291136 :: Nat) Source # | |
Defined in Data.Singletons.Prelude.Show | |
type Apply (TakeSym0 :: TyFun Nat (NonEmpty a6989586621681159612 ~> [a6989586621681159612]) -> Type) (a6989586621681161161 :: Nat) Source # | |
Defined in Data.Singletons.Prelude.List.NonEmpty | |
type Apply (DropSym0 :: TyFun Nat (NonEmpty a6989586621681159611 ~> [a6989586621681159611]) -> Type) (a6989586621681161153 :: Nat) Source # | |
Defined in Data.Singletons.Prelude.List.NonEmpty | |
type Apply (SplitAtSym0 :: TyFun Nat (NonEmpty a6989586621681159610 ~> ([a6989586621681159610], [a6989586621681159610])) -> Type) (a6989586621681161145 :: Nat) Source # | |
Defined in Data.Singletons.Prelude.List.NonEmpty type Apply (SplitAtSym0 :: TyFun Nat (NonEmpty a6989586621681159610 ~> ([a6989586621681159610], [a6989586621681159610])) -> Type) (a6989586621681161145 :: Nat) = SplitAtSym1 a6989586621681161145 a6989586621681159610 :: TyFun (NonEmpty a6989586621681159610) ([a6989586621681159610], [a6989586621681159610]) -> Type | |
type Apply (ElemIndicesSym0 :: TyFun a6989586621679970167 ([a6989586621679970167] ~> [Nat]) -> Type) (a6989586621679974701 :: a6989586621679970167) Source # | |
Defined in Data.Singletons.Prelude.List.Internal type Apply (ElemIndicesSym0 :: TyFun a6989586621679970167 ([a6989586621679970167] ~> [Nat]) -> Type) (a6989586621679974701 :: a6989586621679970167) = ElemIndicesSym1 a6989586621679974701 | |
type Apply (ElemIndexSym0 :: TyFun a6989586621679970168 ([a6989586621679970168] ~> Maybe Nat) -> Type) (a6989586621679974709 :: a6989586621679970168) Source # | |
Defined in Data.Singletons.Prelude.List.Internal type Apply (ElemIndexSym0 :: TyFun a6989586621679970168 ([a6989586621679970168] ~> Maybe Nat) -> Type) (a6989586621679974709 :: a6989586621679970168) = ElemIndexSym1 a6989586621679974709 | |
type Apply (ReplicateM_Sym0 :: TyFun Nat (m6989586621681270963 a6989586621681270964 ~> m6989586621681270963 ()) -> Type) (a6989586621681271323 :: Nat) Source # | |
Defined in Data.Singletons.Prelude.Monad type Apply (ReplicateM_Sym0 :: TyFun Nat (m6989586621681270963 a6989586621681270964 ~> m6989586621681270963 ()) -> Type) (a6989586621681271323 :: Nat) = ReplicateM_Sym1 a6989586621681271323 m6989586621681270963 a6989586621681270964 :: TyFun (m6989586621681270963 a6989586621681270964) (m6989586621681270963 ()) -> Type | |
type Apply (ReplicateMSym0 :: TyFun Nat (m6989586621681270965 a6989586621681270966 ~> m6989586621681270965 [a6989586621681270966]) -> Type) (a6989586621681271342 :: Nat) Source # | |
Defined in Data.Singletons.Prelude.Monad type Apply (ReplicateMSym0 :: TyFun Nat (m6989586621681270965 a6989586621681270966 ~> m6989586621681270965 [a6989586621681270966]) -> Type) (a6989586621681271342 :: Nat) = ReplicateMSym1 a6989586621681271342 m6989586621681270965 a6989586621681270966 :: TyFun (m6989586621681270965 a6989586621681270966) (m6989586621681270965 [a6989586621681270966]) -> Type | |
type Apply (LengthSym0 :: TyFun (NonEmpty a) Nat -> Type) (a6989586621681161362 :: NonEmpty a) Source # | |
Defined in Data.Singletons.Prelude.List.NonEmpty type Apply (LengthSym0 :: TyFun (NonEmpty a) Nat -> Type) (a6989586621681161362 :: NonEmpty a) = Length a6989586621681161362 | |
type Apply (LengthSym0 :: TyFun (t a) Nat -> Type) (arg6989586621680487240 :: t a) Source # | |
Defined in Data.Singletons.Prelude.Foldable type Apply (LengthSym0 :: TyFun (t a) Nat -> Type) (arg6989586621680487240 :: t a) = Length arg6989586621680487240 | |
type Apply (FindIndicesSym1 a6989586621679974667 :: TyFun [a] [Nat] -> Type) (a6989586621679974668 :: [a]) Source # | |
Defined in Data.Singletons.Prelude.List.Internal type Apply (FindIndicesSym1 a6989586621679974667 :: TyFun [a] [Nat] -> Type) (a6989586621679974668 :: [a]) = FindIndices a6989586621679974667 a6989586621679974668 | |
type Apply (ElemIndicesSym1 a6989586621679974701 :: TyFun [a] [Nat] -> Type) (a6989586621679974702 :: [a]) Source # | |
Defined in Data.Singletons.Prelude.List.Internal type Apply (ElemIndicesSym1 a6989586621679974701 :: TyFun [a] [Nat] -> Type) (a6989586621679974702 :: [a]) = ElemIndices a6989586621679974701 a6989586621679974702 | |
type Apply (FindIndexSym1 a6989586621679974693 :: TyFun [a] (Maybe Nat) -> Type) (a6989586621679974694 :: [a]) Source # | |
Defined in Data.Singletons.Prelude.List.Internal type Apply (FindIndexSym1 a6989586621679974693 :: TyFun [a] (Maybe Nat) -> Type) (a6989586621679974694 :: [a]) = FindIndex a6989586621679974693 a6989586621679974694 | |
type Apply (ElemIndexSym1 a6989586621679974709 :: TyFun [a] (Maybe Nat) -> Type) (a6989586621679974710 :: [a]) Source # | |
Defined in Data.Singletons.Prelude.List.Internal type Apply (ElemIndexSym1 a6989586621679974709 :: TyFun [a] (Maybe Nat) -> Type) (a6989586621679974710 :: [a]) = ElemIndex a6989586621679974709 a6989586621679974710 | |
type Apply ((!!@#@$) :: TyFun [a6989586621679970139] (Nat ~> a6989586621679970139) -> Type) (a6989586621679974286 :: [a6989586621679970139]) Source # | |
type Apply ((!!@#@$) :: TyFun (NonEmpty a6989586621681159590) (Nat ~> a6989586621681159590) -> Type) (a6989586621681160950 :: NonEmpty a6989586621681159590) Source # | |
type Apply (FindIndicesSym0 :: TyFun (a6989586621679970165 ~> Bool) ([a6989586621679970165] ~> [Nat]) -> Type) (a6989586621679974667 :: a6989586621679970165 ~> Bool) Source # | |
Defined in Data.Singletons.Prelude.List.Internal type Apply (FindIndicesSym0 :: TyFun (a6989586621679970165 ~> Bool) ([a6989586621679970165] ~> [Nat]) -> Type) (a6989586621679974667 :: a6989586621679970165 ~> Bool) = FindIndicesSym1 a6989586621679974667 | |
type Apply (FindIndexSym0 :: TyFun (a6989586621679970166 ~> Bool) ([a6989586621679970166] ~> Maybe Nat) -> Type) (a6989586621679974693 :: a6989586621679970166 ~> Bool) Source # | |
Defined in Data.Singletons.Prelude.List.Internal type Apply (FindIndexSym0 :: TyFun (a6989586621679970166 ~> Bool) ([a6989586621679970166] ~> Maybe Nat) -> Type) (a6989586621679974693 :: a6989586621679970166 ~> Bool) = FindIndexSym1 a6989586621679974693 |
Instances
type family Sing :: k -> Type Source #
The singleton kind-indexed type family.
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
.
class KnownSymbol (n :: Symbol) #
Minimal complete definition
symbolSing
symbolVal :: forall (n :: Symbol) proxy. KnownSymbol n => proxy n -> String #
(%<=?) :: 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 QuotRem (a :: Nat) (a :: Nat) :: (Nat, Nat) where ... Source #
Equations
QuotRem a_6989586621679504157 a_6989586621679504159 = Apply (Apply DivModSym0 a_6989586621679504157) a_6989586621679504159 |
Defunctionalization symbols
data ErrorSym0 :: forall k06989586621679481870 k6989586621679481871. (~>) k06989586621679481870 k6989586621679481871 Source #
Instances
SingI (ErrorSym0 :: TyFun Symbol a -> Type) Source # | |
SuppressUnusedWarnings (ErrorSym0 :: TyFun k06989586621679481870 k6989586621679481871 -> Type) Source # | |
Defined in Data.Singletons.TypeLits.Internal Methods suppressUnusedWarnings :: () Source # | |
type Apply (ErrorSym0 :: TyFun k0 k2 -> Type) (str6989586621679481872 :: k0) Source # | |
Defined in Data.Singletons.TypeLits.Internal |
type ErrorSym1 (str6989586621679481872 :: k06989586621679481870) = Error str6989586621679481872 Source #
data ErrorWithoutStackTraceSym0 :: forall k06989586621679482960 k6989586621679482961. (~>) k06989586621679482960 k6989586621679482961 Source #
Instances
SingI (ErrorWithoutStackTraceSym0 :: TyFun Symbol a -> Type) Source # | |
Defined in Data.Singletons.TypeLits.Internal Methods | |
SuppressUnusedWarnings (ErrorWithoutStackTraceSym0 :: TyFun k06989586621679482960 k6989586621679482961 -> Type) Source # | |
Defined in Data.Singletons.TypeLits.Internal Methods suppressUnusedWarnings :: () Source # | |
type Apply (ErrorWithoutStackTraceSym0 :: TyFun k0 k2 -> Type) (str6989586621679482962 :: k0) Source # | |
Defined in Data.Singletons.TypeLits.Internal type Apply (ErrorWithoutStackTraceSym0 :: TyFun k0 k2 -> Type) (str6989586621679482962 :: k0) = ErrorWithoutStackTrace str6989586621679482962 :: k2 |
type ErrorWithoutStackTraceSym1 (str6989586621679482962 :: k06989586621679482960) = ErrorWithoutStackTrace str6989586621679482962 Source #
type UndefinedSym0 = Undefined Source #
data KnownNatSym0 :: (~>) Nat Constraint Source #
Instances
SuppressUnusedWarnings KnownNatSym0 Source # | |
Defined in Data.Singletons.TypeLits Methods suppressUnusedWarnings :: () Source # | |
type Apply KnownNatSym0 (n6989586621679482027 :: Nat) Source # | |
Defined in Data.Singletons.TypeLits |
type KnownNatSym1 (n6989586621679482027 :: Nat) = KnownNat n6989586621679482027 Source #
data KnownSymbolSym0 :: (~>) Symbol Constraint Source #
Instances
SuppressUnusedWarnings KnownSymbolSym0 Source # | |
Defined in Data.Singletons.TypeLits Methods suppressUnusedWarnings :: () Source # | |
type Apply KnownSymbolSym0 (n6989586621679482093 :: Symbol) Source # | |
Defined in Data.Singletons.TypeLits |
type KnownSymbolSym1 (n6989586621679482093 :: Symbol) = KnownSymbol n6989586621679482093 Source #
data (^@#@$) :: (~>) Nat ((~>) Nat Nat) infixr 8 Source #
Instances
SingI (^@#@$) Source # | |
SuppressUnusedWarnings (^@#@$) Source # | |
Defined in Data.Singletons.TypeLits.Internal Methods 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 Methods 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 Methods 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 Methods sing :: Sing ((<=?@#@$$) x) Source # | |
SuppressUnusedWarnings ((<=?@#@$$) a3530822107858468865 :: TyFun Nat Bool -> Type) Source # | |
Defined in Data.Singletons.TypeLits.Internal Methods 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 Methods 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 Methods 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 Methods 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 Methods 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 Methods 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 Methods suppressUnusedWarnings :: () Source # | |
type Apply DivModSym0 (a6989586621679504167 :: Nat) Source # | |
Defined in Data.Singletons.TypeLits |
data DivModSym1 (a6989586621679504167 :: Nat) :: (~>) Nat (Nat, Nat) Source #
Instances
SuppressUnusedWarnings (DivModSym1 a6989586621679504167 :: TyFun Nat (Nat, Nat) -> Type) Source # | |
Defined in Data.Singletons.TypeLits Methods suppressUnusedWarnings :: () Source # | |
type Apply (DivModSym1 a6989586621679504167 :: TyFun Nat (Nat, Nat) -> Type) (a6989586621679504168 :: Nat) Source # | |
Defined in Data.Singletons.TypeLits |
type DivModSym2 (a6989586621679504167 :: Nat) (a6989586621679504168 :: Nat) = DivMod a6989586621679504167 a6989586621679504168 Source #
data QuotSym0 :: (~>) Nat ((~>) Nat Nat) infixl 7 Source #
Instances
SuppressUnusedWarnings QuotSym0 Source # | |
Defined in Data.Singletons.TypeLits Methods suppressUnusedWarnings :: () Source # | |
type Apply QuotSym0 (a6989586621679504151 :: Nat) Source # | |
Defined in Data.Singletons.TypeLits |
data QuotSym1 (a6989586621679504151 :: Nat) :: (~>) Nat Nat infixl 7 Source #
type QuotSym2 (a6989586621679504151 :: Nat) (a6989586621679504152 :: Nat) = Quot a6989586621679504151 a6989586621679504152 Source #
data RemSym0 :: (~>) Nat ((~>) Nat Nat) infixl 7 Source #
Instances
SuppressUnusedWarnings RemSym0 Source # | |
Defined in Data.Singletons.TypeLits Methods suppressUnusedWarnings :: () Source # | |
type Apply RemSym0 (a6989586621679504141 :: Nat) Source # | |
Defined in Data.Singletons.TypeLits |
data RemSym1 (a6989586621679504141 :: Nat) :: (~>) Nat Nat infixl 7 Source #
type RemSym2 (a6989586621679504141 :: Nat) (a6989586621679504142 :: Nat) = Rem a6989586621679504141 a6989586621679504142 Source #
data QuotRemSym0 :: (~>) Nat ((~>) Nat (Nat, Nat)) Source #
Instances
SuppressUnusedWarnings QuotRemSym0 Source # | |
Defined in Data.Singletons.TypeLits Methods suppressUnusedWarnings :: () Source # | |
type Apply QuotRemSym0 (a6989586621679504161 :: Nat) Source # | |
Defined in Data.Singletons.TypeLits |
data QuotRemSym1 (a6989586621679504161 :: Nat) :: (~>) Nat (Nat, Nat) Source #
Instances
SuppressUnusedWarnings (QuotRemSym1 a6989586621679504161 :: TyFun Nat (Nat, Nat) -> Type) Source # | |
Defined in Data.Singletons.TypeLits Methods suppressUnusedWarnings :: () Source # | |
type Apply (QuotRemSym1 a6989586621679504161 :: TyFun Nat (Nat, Nat) -> Type) (a6989586621679504162 :: Nat) Source # | |
Defined in Data.Singletons.TypeLits |
type QuotRemSym2 (a6989586621679504161 :: Nat) (a6989586621679504162 :: Nat) = QuotRem a6989586621679504161 a6989586621679504162 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 # | |
Methods fromString :: String -> Symbol | |
Semigroup Symbol Source # | |
Monoid Symbol Source # | |