base-4.12.0.0: Basic libraries
Safe HaskellTrustworthy
LanguageHaskell2010

GHC.TypeNats

Contents

Description

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

Nat Kind

data Nat Source #

(Kind) This is the kind of type-level natural numbers.

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

Minimal complete definition

natSing

natVal :: forall (n :: Nat) proxy. KnownNat n => proxy n -> Natural Source #

Since: base-4.10.0.0

natVal' :: forall (n :: Nat). KnownNat n => Proxy# n -> Natural Source #

Since: base-4.10.0.0

data SomeNat Source #

This type represents unknown type-level natural numbers.

Since: base-4.10.0.0

Constructors

KnownNat n => SomeNat (Proxy n) 
Instances
Eq SomeNat

Since: base-4.7.0.0

Instance details

Defined in GHC.TypeNats

Methods

(==) :: SomeNat -> SomeNat -> Bool Source #

(/=) :: SomeNat -> SomeNat -> Bool Source #

Ord SomeNat

Since: base-4.7.0.0

Instance details

Defined in GHC.TypeNats

Methods

compare :: SomeNat -> SomeNat -> Ordering Source #

(<) :: SomeNat -> SomeNat -> Bool Source #

(<=) :: SomeNat -> SomeNat -> Bool Source #

(>) :: SomeNat -> SomeNat -> Bool Source #

(>=) :: SomeNat -> SomeNat -> Bool Source #

max :: SomeNat -> SomeNat -> SomeNat Source #

min :: SomeNat -> SomeNat -> SomeNat Source #

Read SomeNat

Since: base-4.7.0.0

Instance details

Defined in GHC.TypeNats

Methods

readsPrec :: Int -> ReadS SomeNat Source #

readList :: ReadS [SomeNat] Source #

readPrec :: ReadPrec SomeNat Source #

readListPrec :: ReadPrec [SomeNat] Source #

Show SomeNat

Since: base-4.7.0.0

Instance details

Defined in GHC.TypeNats

Methods

showsPrec :: Int -> SomeNat -> ShowS Source #

show :: SomeNat -> String Source #

showList :: [SomeNat] -> ShowS Source #

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

type family Mod (a :: Nat) (b :: Nat) :: Nat where ... infixl 7 Source #

Modulus of natural numbers. Mod x 0 is undefined (i.e., it cannot be reduced).

Since: base-4.11.0.0

type family Log2 (a :: Nat) :: Nat where ... Source #

Log base 2 (round down) of natural numbers. Log 0 is undefined (i.e., it cannot be reduced).

Since: base-4.11.0.0