Moduleconstraints-0.14.4Haskell2010

Data.Constraint.Nat

Utilities for working with KnownNat constraints.

This module is only available on GHC 8.0 or later.

Synopsis

family Min
family Max
family Lcm
family Gcd
type Divides
family Div
family Mod
family Log2
value plusNat
value minusNat
value timesNat
value powNat
value minNat
value maxNat
value gcdNat
value lcmNat
value divNat
value modNat
value log2Nat
value plusZero
value minusZero
value timesZero
value timesOne
value powZero
value powOne
value maxZero
value minZero
value gcdZero
value gcdOne
value lcmZero
value lcmOne
value plusAssociates
value timesAssociates
value minAssociates
value maxAssociates
value gcdAssociates
value lcmAssociates
value plusCommutes
value timesCommutes
value minCommutes
value maxCommutes
value gcdCommutes
value lcmCommutes
value plusDistributesOverTimes
value timesDistributesOverPow
value timesDistributesOverGcd
value timesDistributesOverLcm
value minDistributesOverPlus
value minDistributesOverTimes
value minDistributesOverPow1
value minDistributesOverPow2
value minDistributesOverMax
value maxDistributesOverPlus
value maxDistributesOverTimes
value maxDistributesOverPow1
value maxDistributesOverPow2
value maxDistributesOverMin
value gcdDistributesOverLcm
value lcmDistributesOverGcd
value minIsIdempotent
value maxIsIdempotent
value lcmIsIdempotent
value gcdIsIdempotent
value plusIsCancellative
value timesIsCancellative
value dividesPlus
value dividesTimes
value dividesMin
value dividesMax
value dividesPow
value dividesGcd
value dividesLcm
value plusMonotone1
value plusMonotone2
value timesMonotone1
value timesMonotone2
value powMonotone1
value powMonotone2
value minMonotone1
value minMonotone2
value maxMonotone1
value maxMonotone2
value divMonotone1
value divMonotone2
value euclideanNat
value plusMod
value timesMod
value modBound
value log2Pow
value dividesDef
value timesDiv
value eqLe
value leEq
value leId
value leTrans
value leZero
value zeroLe
value plusMinusInverse1
value plusMinusInverse2
value plusMinusInverse3

Packageconstraints-0.14.4
Exports100
LanguageHaskell2010
LicenceBSD-2-Clause
SourceNat.hs

familytype family Min (m :: Nat) (n :: Nat) :: Nat where

Equations

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

familytype family Max (m :: Nat) (n :: Nat) :: Nat where

Equations

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

familytype family Lcm (m :: Nat) (n :: Nat) :: Nat where

Equations

Lcm m m = m

familytype family Gcd (m :: Nat) (n :: Nat) :: Nat where

Equations

Gcd m m = m

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

familytype family Div (a :: Natural) (b :: Natural) :: Natural

Source#

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

familytype family Mod (a :: Natural) (b :: Natural) :: Natural

Source#

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

familytype family Log2 (a :: Natural) :: Natural

Source#

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

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

valueminusNat :: (KnownNat n, KnownNat m, m <= n) :- KnownNat (n - m)

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

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

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

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

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

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

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

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

valuelog2Nat :: (KnownNat n, 1 <= n) :- KnownNat (Log2 n)

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

valueminusZero :: Dict ((n - 0) ~ n)

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

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

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

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

valuemaxZero :: Dict (Max n 0 ~ n)

valueminZero :: Dict (Min n 0 ~ 0)

valuegcdZero :: Dict (Gcd 0 a ~ a)

valuegcdOne :: Dict (Gcd 1 a ~ 1)

valuelcmZero :: Dict (Lcm 0 a ~ 0)

valuelcmOne :: Dict (Lcm 1 a ~ a)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

valueminIsIdempotent :: Dict (Min n n ~ n)

valuemaxIsIdempotent :: Dict (Max n n ~ n)

valuelcmIsIdempotent :: Dict (Lcm n n ~ n)

valuegcdIsIdempotent :: Dict (Gcd n n ~ n)

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

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

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

valuedividesTimes :: Divides a b :- Divides a (b * c)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

valuelog2Pow :: Dict (Log2 (2 ^ n) ~ n)

valuedividesDef :: Divides a b :- (Mod b a ~ 0)

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

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

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

valueleId :: Dict (a <= a)

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

valueleZero :: (a <= 0) :- (a ~ 0)

valuezeroLe :: Dict (0 <= a)

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

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

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