Safe Haskell | None |
---|---|
Language | Haskell2010 |
- 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 k (a :: k) :: *
- class PNum a
- class SNum a
- data SSym0 (l :: TyFun Nat Nat) = SameKind (Apply SSym0 arg) (SSym1 arg) => SSym0KindInference
- type SSym1 (t :: Nat) = S t
- type ZSym0 = Z
- type family Lit n where ...
- data LitSym0 (l :: TyFun Nat Nat) = SameKind (Apply LitSym0 arg) (LitSym1 arg) => LitSym0KindInference
- type LitSym1 (t :: Nat) = Lit t
- type SLit n = Sing (Lit n)
- sLit :: forall (n :: Nat). SingI (Lit n) => Sing (Lit n)
Documentation
data family Sing k (a :: k) :: * #
The singleton kind-indexed data family.
Eq (SNat n) # | |
Ord (SNat n) # | |
Show (Sing Nat n) # | |
data Sing Bool | |
data Sing Ordering | |
data Sing Nat | |
data Sing Symbol | |
data Sing () | |
data Sing Nat # | |
data Sing [a] | |
data Sing (Maybe a) | |
data Sing (NonEmpty a) | |
data Sing (Either a b) | |
data Sing (a, b) | |
data Sing ((~>) k1 k2) | |
data Sing (a, b, c) | |
data Sing (a, b, c, d) | |
data Sing (a, b, c, d, e) | |
data Sing (a, b, c, d, e, f) | |
data Sing (a, b, c, d, e, f, g) | |
data SSym0 (l :: TyFun Nat Nat) Source #
SameKind (Apply SSym0 arg) (SSym1 arg) => SSym0KindInference |
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))