Num.Nat

Nat

data Nat

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

Instances

KnownNat n => Reifies (n :: Nat) Integer

Defined in Data.Reflection

Methods

reflect :: proxy n -> Integer

HasPosition i s t a b => HasAny (i :: Nat) s t a b

Defined in Data.Generics.Product.Any

Methods

the :: Lens s t a b

class KnownNat (n :: Nat)

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 :: KnownNat n => proxy n -> Integer

Since: base-4.7.0.0

natVal' :: KnownNat n => Proxy# n -> Integer

Since: base-4.8.0.0

data SomeNat where

This type represents unknown type-level natural numbers.

Since: base-4.10.0.0

Constructors

SomeNat :: SomeNat

Instances

Eq SomeNat

Since: base-4.7.0.0

Defined in GHC.TypeNats

Methods

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

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

Ord SomeNat

Since: base-4.7.0.0

Defined in GHC.TypeNats

Methods

compare :: SomeNat -> SomeNat -> Ordering

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

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

(>) :: SomeNat -> SomeNat -> Bool

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

max :: SomeNat -> SomeNat -> SomeNat

min :: SomeNat -> SomeNat -> SomeNat

Read SomeNat

Since: base-4.7.0.0

Defined in GHC.TypeNats

Methods

readsPrec :: Int -> ReadS SomeNat

readList :: ReadS [SomeNat]

readPrec :: ReadPrec SomeNat

readListPrec :: ReadPrec [SomeNat]

Show SomeNat

Since: base-4.7.0.0

Defined in GHC.TypeNats

Methods

showsPrec :: Int -> SomeNat -> ShowS

show :: SomeNat -> String

showList :: [SomeNat] -> ShowS

someNatVal :: Integer -> Maybe SomeNat

Convert an integer into an unknown type-level natural.

Since: base-4.7.0.0

sameNat :: (KnownNat a, KnownNat b) => Proxy a -> Proxy b -> Maybe (a :~: b)

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

Since: base-4.7.0.0

type (<=) (x :: Nat) (y :: Nat) = (x <=? y) ~ True infix 4

Comparison of type-level naturals, as a constraint.

Since: base-4.7.0.0

type family (a :: Nat) <=? (b :: Nat) :: Bool where ... infix 4

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

Addition of type-level naturals.

Since: base-4.7.0.0

type family (a :: Nat) * (b :: Nat) :: Nat where ... infixl 7

Multiplication of type-level naturals.

Since: base-4.7.0.0

type family (a :: Nat) ^ (b :: Nat) :: Nat where ... infixr 8

Exponentiation of type-level naturals.

Since: base-4.7.0.0

type family (a :: Nat) - (b :: Nat) :: Nat where ... infixl 6

Subtraction of type-level naturals.

Since: base-4.7.0.0

type family Min (m :: Nat) (n :: Nat) :: Nat where ...

Equations

Min m m = m

type family Max (m :: Nat) (n :: Nat) :: Nat where ...

Equations

Max m m = m

type family Lcm (m :: Nat) (n :: Nat) :: Nat where ...

Equations

Lcm m m = m

type family Gcd (m :: Nat) (n :: Nat) :: Nat where ...

Equations

Gcd m m = m

type Divides (n :: Nat) (m :: Nat) = n ~ Gcd n m

type family Div (a :: Nat) (b :: Nat) :: Nat where ... infixl 7

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

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 ...

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

Since: base-4.11.0.0

type family CmpNat (a :: Nat) (b :: Nat) :: Ordering where ...

Comparison of type-level naturals, as a function.

Since: base-4.7.0.0

Constraints

plusNat :: (KnownNat n, KnownNat m) :- KnownNat (n + m)

timesNat :: (KnownNat n, KnownNat m) :- KnownNat (n * m)

powNat :: (KnownNat n, KnownNat m) :- KnownNat (n ^ m)

minNat :: (KnownNat n, KnownNat m) :- KnownNat (Min n m)

maxNat :: (KnownNat n, KnownNat m) :- KnownNat (Max n m)

gcdNat :: (KnownNat n, KnownNat m) :- KnownNat (Gcd n m)

lcmNat :: (KnownNat n, KnownNat m) :- KnownNat (Lcm n m)

divNat :: (KnownNat n, KnownNat m, 1 <= m) :- KnownNat (Div n m)

modNat :: (KnownNat n, KnownNat m, 1 <= m) :- KnownNat (Mod n m)

plusZero :: Dict ((n + 0) ~ n)

timesZero :: Dict ((n * 0) ~ 0)

timesOne :: Dict ((n * 1) ~ n)

powZero :: Dict ((n ^ 0) ~ 1)

powOne :: Dict ((n ^ 1) ~ n)

maxZero :: Dict (Max n 0 ~ n)

minZero :: Dict (Min n 0 ~ 0)

gcdZero :: Dict (Gcd 0 a ~ a)

gcdOne :: Dict (Gcd 1 a ~ 1)

lcmZero :: Dict (Lcm 0 a ~ 0)

lcmOne :: Dict (Lcm 1 a ~ a)

plusAssociates :: Dict (((m + n) + o) ~ (m + (n + o)))

timesAssociates :: Dict (((m * n) * o) ~ (m * (n * o)))

minAssociates :: Dict (Min (Min m n) o ~ Min m (Min n o))

maxAssociates :: Dict (Max (Max m n) o ~ Max m (Max n o))

gcdAssociates :: Dict (Gcd (Gcd a b) c ~ Gcd a (Gcd b c))

lcmAssociates :: Dict (Lcm (Lcm a b) c ~ Lcm a (Lcm b c))

plusCommutes :: Dict ((m + n) ~ (n + m))

timesCommutes :: Dict ((m * n) ~ (n * m))

minCommutes :: Dict (Min m n ~ Min n m)

maxCommutes :: Dict (Max m n ~ Max n m)

gcdCommutes :: Dict (Gcd a b ~ Gcd b a)

lcmCommutes :: Dict (Lcm a b ~ Lcm b a)

plusDistributesOverTimes :: Dict ((n * (m + o)) ~ ((n * m) + (n * o)))

timesDistributesOverPow :: Dict ((n ^ (m + o)) ~ ((n ^ m) * (n ^ o)))

timesDistributesOverGcd :: Dict ((n * Gcd m o) ~ Gcd (n * m) (n * o))

timesDistributesOverLcm :: Dict ((n * Lcm m o) ~ Lcm (n * m) (n * o))

minDistributesOverPlus :: Dict ((n + Min m o) ~ Min (n + m) (n + o))

minDistributesOverTimes :: Dict ((n * Min m o) ~ Min (n * m) (n * o))

minDistributesOverPow1 :: Dict ((Min n m ^ o) ~ Min (n ^ o) (m ^ o))

minDistributesOverPow2 :: Dict ((n ^ Min m o) ~ Min (n ^ m) (n ^ o))

minDistributesOverMax :: Dict (Max n (Min m o) ~ Min (Max n m) (Max n o))

maxDistributesOverPlus :: Dict ((n + Max m o) ~ Max (n + m) (n + o))

maxDistributesOverTimes :: Dict ((n * Max m o) ~ Max (n * m) (n * o))

maxDistributesOverPow1 :: Dict ((Max n m ^ o) ~ Max (n ^ o) (m ^ o))

maxDistributesOverPow2 :: Dict ((n ^ Max m o) ~ Max (n ^ m) (n ^ o))

maxDistributesOverMin :: Dict (Min n (Max m o) ~ Max (Min n m) (Min n o))

gcdDistributesOverLcm :: Dict (Gcd (Lcm a b) c ~ Lcm (Gcd a c) (Gcd b c))

lcmDistributesOverGcd :: Dict (Lcm (Gcd a b) c ~ Gcd (Lcm a c) (Lcm b c))

minIsIdempotent :: Dict (Min n n ~ n)

maxIsIdempotent :: Dict (Max n n ~ n)

lcmIsIdempotent :: Dict (Lcm n n ~ n)

gcdIsIdempotent :: Dict (Gcd n n ~ n)

plusIsCancellative :: ((n + m) ~ (n + o)) :- (m ~ o)

timesIsCancellative :: (1 <= n, (n * m) ~ (n * o)) :- (m ~ o)

dividesPlus :: (Divides a b, Divides a c) :- Divides a (b + c)

dividesTimes :: (Divides a b, Divides a c) :- Divides a (b * c)

dividesMin :: (Divides a b, Divides a c) :- Divides a (Min b c)

dividesMax :: (Divides a b, Divides a c) :- Divides a (Max b c)

dividesPow :: (1 <= n, Divides a b) :- Divides a (b ^ n)

dividesGcd :: (Divides a b, Divides a c) :- Divides a (Gcd b c)

dividesLcm :: (Divides a c, Divides b c) :- Divides (Lcm a b) c

plusMonotone1 :: (a <= b) :- ((a + c) <= (b + c))

plusMonotone2 :: (b <= c) :- ((a + b) <= (a + c))

timesMonotone1 :: (a <= b) :- ((a * c) <= (b * c))

timesMonotone2 :: (b <= c) :- ((a * b) <= (a * c))

powMonotone1 :: (a <= b) :- ((a ^ c) <= (b ^ c))

powMonotone2 :: (b <= c) :- ((a ^ b) <= (a ^ c))

minMonotone1 :: (a <= b) :- (Min a c <= Min b c)

minMonotone2 :: (b <= c) :- (Min a b <= Min a c)

maxMonotone1 :: (a <= b) :- (Max a c <= Max b c)

maxMonotone2 :: (b <= c) :- (Max a b <= Max a c)

divMonotone1 :: (a <= b) :- (Div a c <= Div b c)

divMonotone2 :: (b <= c) :- (Div a c <= Div a b)

euclideanNat :: (1 <= c) :- (a ~ ((c * Div a c) + Mod a c))

plusMod :: (1 <= c) :- (Mod (a + b) c ~ Mod (Mod a c + Mod b c) c)

timesMod :: (1 <= c) :- (Mod (a * b) c ~ Mod (Mod a c * Mod b c) c)

modBound :: (1 <= n) :- (Mod m n <= n)

dividesDef :: Divides a b :- ((a * Div b a) ~ a)

timesDiv :: Dict ((a * Div b a) <= a)

eqLe :: (a ~ b) :- (a <= b)

leEq :: (a <= b, b <= a) :- (a ~ b)

leId :: Dict (a <= a)

leTrans :: (b <= c, a <= b) :- (a <= c)

zeroLe :: Dict (0 <= a)

plusMinusInverse1 :: Dict (((m + n) - n) ~ m)

plusMinusInverse2 :: (m <= n) :- (((m + n) - m) ~ n)

plusMinusInverse3 :: (n <= m) :- (((m - n) + n) ~ m)