Safe Haskell | None |
---|---|
Language | Haskell2010 |
Synopsis
- data Nat
- type family NatPlus (a :: Nat) (a :: Nat) :: Nat where ...
- type family NatMul (a :: Nat) (a :: Nat) :: Nat where ...
- type family NatMinus (a :: Nat) (a :: Nat) :: Nat where ...
- type family NatAbs (a :: Nat) :: Nat where ...
- type family NatSignum (a :: Nat) :: Nat where ...
- natPlus :: Nat -> Nat -> Nat
- natMul :: Nat -> Nat -> Nat
- natMinus :: Nat -> Nat -> Nat
- natAbs :: Nat -> Nat
- natSignum :: Nat -> Nat
- someNatVal :: Integer -> Maybe (SomeSing Nat)
- type SNat = (Sing :: Nat -> Type)
- data family Sing (a :: k) :: Type
- class PNum a
- class SNum a
- data SSym0 :: (~>) Nat Nat where
- type SSym1 (t6989586621679080960 :: Nat) = S t6989586621679080960
- type ZSym0 = Z
- type family Lit n where ...
- data LitSym0 :: (~>) Nat Nat where
- type LitSym1 (n6989586621679094994 :: Nat) = Lit n6989586621679094994
- type SLit n = Sing (Lit n)
- sLit :: forall (n :: Nat). SingI (Lit n) => Sing (Lit n)
Documentation
Instances
data family Sing (a :: k) :: Type #
The singleton kind-indexed data family.
Instances
Eq (SNat n) Source # | |
Ord (SNat n) Source # | |
ShowSing Nat => Show (Sing z) Source # | |
data Sing (a :: Bool) | |
data Sing (a :: Ordering) | |
data Sing (n :: Nat) | |
data Sing (n :: Symbol) | |
Defined in Data.Singletons.TypeLits.Internal | |
data Sing (a :: ()) | |
Defined in Data.Singletons.Prelude.Instances | |
data Sing (a :: Nat) Source # | |
data Sing (a :: Void) | |
Defined in Data.Singletons.Prelude.Instances | |
data Sing (a :: All) | |
data Sing (a :: Any) | |
data Sing (b :: [a]) | |
data Sing (b :: Maybe a) | |
data Sing (b :: Min a) | |
data Sing (b :: Max a) | |
data Sing (b :: First a) | |
data Sing (b :: Last a) | |
data Sing (a :: WrappedMonoid m) | |
Defined in Data.Singletons.Prelude.Semigroup.Internal data Sing (a :: WrappedMonoid m) where
| |
data Sing (b :: Option a) | |
data Sing (b :: Identity a) | |
data Sing (b :: First a) | |
data Sing (b :: Last a) | |
data Sing (b :: Dual a) | |
data Sing (b :: Sum a) | |
data Sing (b :: Product a) | |
data Sing (b :: Down a) | |
data Sing (b :: NonEmpty a) | |
data Sing (b :: Endo a) | |
data Sing (b :: MaxInternal a) | |
Defined in Data.Singletons.Prelude.Foldable data Sing (b :: MaxInternal a) where
| |
data Sing (b :: MinInternal a) | |
Defined in Data.Singletons.Prelude.Foldable data Sing (b :: MinInternal a) where
| |
data Sing (c :: Either a b) | |
data Sing (c :: (a, b)) | |
data Sing (c :: Arg a b) | |
newtype Sing (f :: k1 ~> k2) | |
data Sing (b :: StateL s a) | |
data Sing (b :: StateR s a) | |
data Sing (d :: (a, b, c)) | |
data Sing (c :: Const a b) | |
data Sing (e :: (a, b, c, d)) | |
data Sing (f :: (a, b, c, d, e)) | |
data Sing (g :: (a, b, c, d, e, f)) | |
Defined in Data.Singletons.Prelude.Instances | |
data Sing (h :: (a, b, c, d, e, f, g)) | |
Defined in Data.Singletons.Prelude.Instances |
(%+), (%*), sAbs, sSignum, sFromInteger
Instances
data SSym0 :: (~>) Nat Nat where Source #
SSym0KindInference :: forall t6989586621679080960 arg. SameKind (Apply SSym0 arg) (SSym1 arg) => SSym0 t6989586621679080960 |
type family Lit n where ... Source #
Provides a shorthand for Nat
-s using GHC.TypeLits, for example:
>>>
:kind! Lit 3
Lit 3 :: Nat = 'S ('S ('S 'Z))