Data.Constraint.Nat

Utilities for working with KnownNat constraints.

This module is only available on GHC 8.0 or later.

Documentation

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

Equations

Min m n = If (n <=? m) n m

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

Equations

Max m n = If (n <=? m) m n

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 m = 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

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

minusNat :: forall n m. (KnownNat n, KnownNat m, m <= n) :- KnownNat (n - m)

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

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

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

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

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

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

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

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

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

minusZero :: forall n. Dict ((n - 0) ~ n)

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

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

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

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

maxZero :: forall n. Dict (Max n 0 ~ n)

minZero :: forall n. Dict (Min n 0 ~ 0)

gcdZero :: forall a. Dict (Gcd 0 a ~ a)

gcdOne :: forall a. Dict (Gcd 1 a ~ 1)

lcmZero :: forall a. Dict (Lcm 0 a ~ 0)

lcmOne :: forall a. Dict (Lcm 1 a ~ a)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

minIsIdempotent :: forall n. Dict (Min n n ~ n)

maxIsIdempotent :: forall n. Dict (Max n n ~ n)

lcmIsIdempotent :: forall n. Dict (Lcm n n ~ n)

gcdIsIdempotent :: forall n. Dict (Gcd n n ~ n)

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

timesIsCancellative :: forall n m o. (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 (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 :: forall a b c. (Divides a b, Divides a c) :- Divides a (Gcd b c)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

dividesDef :: forall a b. Divides a b :- (Mod b a ~ 0)

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

eqLe :: forall (a :: Nat) (b :: Nat). (a ~ b) :- (a <= b)

leEq :: forall (a :: Nat) (b :: Nat). (a <= b, b <= a) :- (a ~ b)

leId :: forall (a :: Nat). Dict (a <= a)

leTrans :: forall (a :: Nat) (b :: Nat) (c :: Nat). (b <= c, a <= b) :- (a <= c)

leZero :: forall a. (a <= 0) :- (a ~ 0)

zeroLe :: forall (a :: Nat). Dict (0 <= a)

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

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

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