Data.Constraint.Nat · constraints-0.14.4

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

#

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

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

#

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

#

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