Moduleconstraints-0.14.4

Data.Constraint.Nat

Synopsis

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

Packageconstraints-0.14.4
Exports100
LicenceBSD-2-Clause
SourceTypeNats.hs

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

valuegcdIsIdempotent :: Dict (Gcd n n ~ n)

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

valuegcdOne :: Dict (Gcd 1 a ~ 1)

valuegcdZero :: Dict (Gcd 0 a ~ a)

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

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

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

valuelcmIsIdempotent :: Dict (Lcm n n ~ n)

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

valuelcmOne :: Dict (Lcm 1 a ~ a)

valuelcmZero :: Dict (Lcm 0 a ~ 0)

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

valueleId :: Dict (a <= a)

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

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

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

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

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

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

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

valuemaxDistributesOverPlus :: 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))

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

valuemaxIsIdempotent :: Dict (Max n n ~ n)

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

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

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

valuemaxZero :: Dict (Max n 0 ~ n)

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

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

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

valueminDistributesOverPlus :: 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))

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

valueminIsIdempotent :: Dict (Min n n ~ n)

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

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

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

valueminZero :: Dict (Min n 0 ~ 0)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

valuezeroLe :: Dict (0 <= a)

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

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

Equations

Gcd m m = m

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

Equations

Lcm m m = m

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

Equations

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

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

Equations

Min m n = If (n <=? m) 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 Log2 (a :: Natural) :: Natural

Source#

Log base 2 (round down) of natural numbers. Log 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).