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: 4.10.0.0
(Kind) This is the kind of type-level natural numbers.
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: 4.7.0.0
natSing
natVal :: forall n proxy. KnownNat n => proxy n -> Natural Source
Since: 4.10.0.0
natVal' :: forall n. KnownNat n => Proxy# n -> Natural Source
Since: 4.10.0.0
This type represents unknown type-level natural numbers.
Since: 4.10.0.0
someNatVal :: Natural -> SomeNat Source
Convert an integer into an unknown type-level natural.
Since: 4.10.0.0
sameNat :: (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: 4.7.0.0
type (<=) x y = (x <=? y) ~ True infix 4 Source
Comparison of type-level naturals, as a constraint.
type family (m :: Nat) <=? (n :: Nat) :: Bool 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 (m :: Nat) + (n :: Nat) :: Nat infixl 6 Source
Addition of type-level naturals.
type family (m :: Nat) * (n :: Nat) :: Nat infixl 7 Source
Multiplication of type-level naturals.
type family (m :: Nat) ^ (n :: Nat) :: Nat infixr 8 Source
Exponentiation of type-level naturals.
type family (m :: Nat) - (n :: Nat) :: Nat infixl 6 Source
Subtraction of type-level naturals.
Since: 4.7.0.0
type family CmpNat (m :: Nat) (n :: Nat) :: Ordering Source
Comparison of type-level naturals, as a function.
Since: 4.7.0.0
© The University of Glasgow and others
Licensed under a BSD-style license (see top of the page).
https://downloads.haskell.org/~ghc/8.2.1/docs/html/libraries/base-4.10.0.0/GHC-TypeNats.html