GHC.TypeNats

Natural number

Invariant: numbers <= 0xffffffffffffffff use the NS constructor

Exponentiation of type-level naturals.

Multiplication of type-level naturals.

Addition of type-level naturals.

Comparison (<=) of comparable types, as a constraint.

Subtraction of type-level naturals.

A type synonym for Natural.

Previously, this was an opaque data type, but it was changed to a type synonym.

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.

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

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

Division (round down) of natural numbers. Div x 0 is undefined (i.e., it cannot be reduced).

A value-level witness for a type-level natural number. This is commonly referred to as a singleton type, as for each n, there is a single value that inhabits the type SNat n (aside from bottom).

The definition of SNat is intentionally left abstract. To obtain an SNat value, use one of the following:

1. The natSing method of KnownNat.

2. The SNat pattern synonym.

3. The withSomeSNat function, which creates an SNat from a Natural number.

A explicitly bidirectional pattern synonym relating an SNat to a KnownNat constraint.

As an expression: Constructs an explicit SNat n value from an implicit KnownNat n constraint:

SNat @n :: KnownNat n => SNat n

As a pattern: Matches on an explicit SNat n value bringing an implicit KnownNat n constraint into scope:

f :: SNat n -> ..
f SNat = {- KnownNat n in scope -}

Like sameNat, but if the numbers aren't equal, this additionally provides proof of LT or GT.

We either get evidence that this function was instantiated with the same type-level numbers, or that the type-level numbers are distinct.

Return the Natural number corresponding to n in an SNat n value.

We either get evidence that this function was instantiated with the same type-level numbers, or Nothing.

Convert an integer into an unknown type-level natural.

Convert an explicit SNat n value into an implicit KnownNat n constraint.

Convert a Natural number into an SNat n value, where n is a fresh type-level natural number.

Comparison (<=) of comparable types, as a function.

This type represents unknown type-level natural numbers.

Comparison of type-level naturals, as a function.