Safe Haskell | Trustworthy |
---|---|
Language | Haskell2010 |
This module is an internal GHC module. It declares the constants used in the implementation of type-level natural numbers. The programmer interface for working with type-level naturals should be defined in a separate library.
Since: base-4.10.0.0
Synopsis
- data Nat
- class KnownNat (n :: Nat)
- natVal :: forall (n :: Nat) proxy. KnownNat n => proxy n -> Natural
- natVal' :: forall (n :: Nat). KnownNat n => Proxy# n -> Natural
- data SomeNat = KnownNat n => SomeNat (Proxy n)
- someNatVal :: Natural -> SomeNat
- sameNat :: forall (a :: Nat) (b :: Nat). (KnownNat a, KnownNat b) => Proxy a -> Proxy b -> Maybe (a :~: b)
- type (<=) (x :: Nat) (y :: Nat) = (x <=? y) ~ True
- type family (a :: Nat) <=? (b :: Nat) :: Bool where ...
- type family (a :: Nat) + (b :: Nat) :: Nat where ...
- type family (a :: Nat) * (b :: Nat) :: Nat where ...
- type family (a :: Nat) ^ (b :: Nat) :: Nat where ...
- type family (a :: Nat) - (b :: Nat) :: Nat where ...
- type family CmpNat (a :: Nat) (b :: Nat) :: Ordering where ...
- type family Div (a :: Nat) (b :: Nat) :: Nat where ...
- type family Mod (a :: Nat) (b :: Nat) :: Nat where ...
- type family Log2 (a :: Nat) :: Nat where ...
Nat Kind
Linking type and value level
class KnownNat (n :: Nat) Source #
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
natSing
This type represents unknown type-level natural numbers.
Since: base-4.10.0.0
Instances
Eq SomeNat | Since: base-4.7.0.0 |
Ord SomeNat | Since: base-4.7.0.0 |
Read SomeNat | Since: base-4.7.0.0 |
Show SomeNat | Since: base-4.7.0.0 |
someNatVal :: Natural -> SomeNat Source #
Convert an integer into an unknown type-level natural.
Since: base-4.10.0.0
sameNat :: forall (a :: Nat) (b :: Nat). (KnownNat a, KnownNat b) => Proxy a -> Proxy b -> Maybe (a :~: b) Source #
We either get evidence that this function was instantiated with the
same type-level numbers, or Nothing
.
Since: base-4.7.0.0
Functions on type literals
type (<=) (x :: Nat) (y :: Nat) = (x <=? y) ~ True infix 4 Source #
Comparison of type-level naturals, as a constraint.
Since: base-4.7.0.0
type family (a :: Nat) <=? (b :: Nat) :: Bool where ... infix 4 Source #
Comparison of type-level naturals, as a function.
NOTE: The functionality for this function should be subsumed
by CmpNat
, so this might go away in the future.
Please let us know, if you encounter discrepancies between the two.
type family (a :: Nat) + (b :: Nat) :: Nat where ... infixl 6 Source #
Addition of type-level naturals.
Since: base-4.7.0.0
type family (a :: Nat) * (b :: Nat) :: Nat where ... infixl 7 Source #
Multiplication of type-level naturals.
Since: base-4.7.0.0
type family (a :: Nat) ^ (b :: Nat) :: Nat where ... infixr 8 Source #
Exponentiation of type-level naturals.
Since: base-4.7.0.0
type family (a :: Nat) - (b :: Nat) :: Nat where ... infixl 6 Source #
Subtraction of type-level naturals.
Since: base-4.7.0.0
type family CmpNat (a :: Nat) (b :: Nat) :: Ordering where ... Source #
Comparison of type-level naturals, as a function.
Since: base-4.7.0.0
type family Div (a :: Nat) (b :: Nat) :: Nat where ... infixl 7 Source #
Division (round down) of natural numbers.
Div x 0
is undefined (i.e., it cannot be reduced).
Since: base-4.11.0.0